Nuprl Lemma : injection-if-compose-injection

[T:Type]. ∀[f,g:T ⟶ T].  Inj(T;T;f) supposing Inj(T;T;g f)


Proof




Definitions occuring in Statement :  inject: Inj(A;B;f) compose: g uimplies: supposing a uall: [x:A]. B[x] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a compose: g inject: Inj(A;B;f) all: x:A. B[x] implies:  Q prop: guard: {T} squash: T true: True subtype_rel: A ⊆B iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q
Lemmas referenced :  equal_wf inject_wf compose_wf squash_wf true_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution sqequalRule lambdaFormation hypothesis extract_by_obid isectElimination thin cumulativity hypothesisEquality applyEquality functionExtensionality because_Cache lambdaEquality dependent_functionElimination axiomEquality isect_memberEquality equalityTransitivity equalitySymmetry functionEquality universeEquality imageElimination natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[f,g:T  {}\mrightarrow{}  T].    Inj(T;T;f)  supposing  Inj(T;T;g  o  f)



Date html generated: 2017_04_14-AM-07_34_15
Last ObjectModification: 2017_02_27-PM-03_07_27

Theory : fun_1


Home Index