Nuprl Lemma : toptype_wf
∀[X:Space]. (|X| ∈ Type)
Proof
Definitions occuring in Statement :
toptype: |X|,
topspace: Space,
uall: ∀[x:A]. B[x],
member: t ∈ T,
universe: Type
Definitions unfolded in proof :
top: Top,
topspace: Space,
toptype: |X|,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
topspace_wf,
pi1_wf_top
Rules used in proof :
equalitySymmetry,
equalityTransitivity,
axiomEquality,
hypothesis,
voidEquality,
voidElimination,
isect_memberEquality,
hypothesisEquality,
independent_pairEquality,
productElimination,
universeEquality,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
instantiate,
thin,
sqequalRule,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[X:Space]. (|X| \mmember{} Type)
Date html generated:
2018_07_29-AM-09_47_39
Last ObjectModification:
2018_06_21-AM-10_02_55
Theory : inner!product!spaces
Home
Index