### Nuprl Lemma : update_wf

`∀[A,B:Type]. ∀[eq:A ⟶ A ⟶ 𝔹]. ∀[f:A ⟶ B]. ∀[x:A]. ∀[v:B].  (f[x:=v] ∈ A ⟶ B)`

Proof

Definitions occuring in Statement :  update: `f[x:=v]` bool: `𝔹` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  update: `f[x:=v]` uall: `∀[x:A]. B[x]` member: `t ∈ T`
Lemmas referenced :  ifthenelse_wf bool_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lambdaEquality lemma_by_obid sqequalHypSubstitution isectElimination thin applyEquality hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache functionEquality universeEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[eq:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[x:A].  \mforall{}[v:B].    (f[x:=v]  \mmember{}  A  {}\mrightarrow{}  B)

Date html generated: 2016_05_15-PM-03_49_13
Last ObjectModification: 2015_12_27-PM-01_22_00

Theory : general

Home Index