### Nuprl Lemma : strict-fun

`∀[f:Base]. f ∈ partial(Void) ⟶ partial(Void) supposing f ⊥ ~ ⊥`

Proof

Definitions occuring in Statement :  partial: `partial(T)` bottom: `⊥` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` member: `t ∈ T` apply: `f a` function: `x:A ⟶ B[x]` base: `Base` void: `Void` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` all: `∀x:A. B[x]`
Lemmas referenced :  partial-void bottom_wf-partial void-value-type partial_wf base_sq base_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut functionExtensionality lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis sqequalRule isectElimination voidEquality independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry sqequalIntensionalEquality isect_memberEquality because_Cache

Latex:
\mforall{}[f:Base].  f  \mmember{}  partial(Void)  {}\mrightarrow{}  partial(Void)  supposing  f  \mbot{}  \msim{}  \mbot{}

Date html generated: 2016_05_14-AM-06_11_19
Last ObjectModification: 2015_12_26-AM-11_51_44

Theory : partial_1

Home Index