### Nuprl Lemma : retract_wf

`∀[T:Type]. ∀[f:Base].  retract(T;f) ∈ ℙ supposing T ⊆r Base`

Proof

Definitions occuring in Statement :  retract: `retract(T;f)` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` base: `Base` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` retract: `retract(T;f)` subtype_rel: `A ⊆r B` implies: `P `` Q` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  all_wf and_wf has-value_wf_base equal-wf-base base_wf subtype_rel_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry lemma_by_obid isectElimination thin hypothesisEquality isect_memberEquality because_Cache universeEquality baseApply closedConclusion baseClosed applyEquality functionEquality lambdaEquality

Latex:
\mforall{}[T:Type].  \mforall{}[f:Base].    retract(T;f)  \mmember{}  \mBbbP{}  supposing  T  \msubseteq{}r  Base

Date html generated: 2016_05_14-PM-03_31_34
Last ObjectModification: 2016_01_14-PM-11_19_23

Theory : decidable!equality

Home Index