### Nuprl Lemma : injective-quotient-typing

`∀[T,S:Type]. ∀[f:T ⟶ S].  (f ∈ T//x.f[x] ⟶ S)`

Proof

Definitions occuring in Statement :  injective-quotient: `T//x.f[x]` uall: `∀[x:A]. B[x]` so_apply: `x[s]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` so_apply: `x[s]` injective-quotient: `T//x.f[x]` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` prop: `ℙ`
Lemmas referenced :  injective-quotient_wf equal-wf-base equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut functionExtensionality extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality sqequalRule lambdaEquality applyEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry functionEquality isect_memberEquality because_Cache universeEquality pointwiseFunctionalityForEquality pertypeElimination productElimination productEquality

Latex:
\mforall{}[T,S:Type].  \mforall{}[f:T  {}\mrightarrow{}  S].    (f  \mmember{}  T//x.f[x]  {}\mrightarrow{}  S)

Date html generated: 2017_04_14-AM-07_40_08
Last ObjectModification: 2017_02_27-PM-03_11_23

Theory : quot_1

Home Index