Nuprl Lemma : free-1-iso_wf
∀[S:Type]. ∀[s:S]. ∀[K:CRng]. free-1-iso(s;K) ∈ free-vs(K;S) ≅ one-dim-vs(K) supposing ∀x,y:S. (x = y ∈ S)
Proof
Definitions occuring in Statement :
free-1-iso: free-1-iso(s;K),
free-vs: free-vs(K;S),
vs-iso: A ≅ B,
one-dim-vs: one-dim-vs(K),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
member: t ∈ T,
universe: Type,
equal: s = t ∈ T,
crng: CRng
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
free-1-iso: free-1-iso(s;K),
free-vs-dim-1-ext,
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
prop: ℙ,
crng: CRng,
rng: Rng
Lemmas referenced :
free-vs-dim-1-ext,
subtype_rel_self,
crng_wf,
equal_wf,
vs-iso_wf,
free-vs_wf,
one-dim-vs_wf,
subtype_rel_function,
uimplies_subtype,
istype-universe
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
applyEquality,
thin,
instantiate,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
isectElimination,
functionEquality,
universeEquality,
cumulativity,
hypothesisEquality,
isectEquality,
setElimination,
rename,
because_Cache,
independent_isectElimination,
lambdaEquality_alt,
universeIsType,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
functionIsType,
inhabitedIsType,
equalityIstype,
isect_memberEquality_alt,
isectIsTypeImplies
Latex:
\mforall{}[S:Type]. \mforall{}[s:S]. \mforall{}[K:CRng].
free-1-iso(s;K) \mmember{} free-vs(K;S) \mcong{} one-dim-vs(K) supposing \mforall{}x,y:S. (x = y)
Date html generated:
2019_10_31-AM-06_30_57
Last ObjectModification:
2019_08_02-PM-04_39_22
Theory : linear!algebra
Home
Index