Nuprl Lemma : trivial-biject-exists
∀[T:Type]. ∃f:T ⟶ T. Bij(T;T;f)
Proof
Definitions occuring in Statement :
biject: Bij(A;B;f),
uall: ∀[x:A]. B[x],
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
prop: ℙ,
member: t ∈ T,
exists: ∃x:A. B[x],
uall: ∀[x:A]. B[x]
Lemmas referenced :
biject_wf,
id-biject
Rules used in proof :
universeEquality,
applyEquality,
functionExtensionality,
hypothesis,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
cumulativity,
hypothesisEquality,
lambdaEquality,
dependent_pairFormation,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[T:Type]. \mexists{}f:T {}\mrightarrow{} T. Bij(T;T;f)
Date html generated:
2017_09_29-PM-05_58_04
Last ObjectModification:
2017_09_04-PM-00_13_50
Theory : list_1
Home
Index