Nuprl Lemma : euclidean-plane-subtype
EuclideanPlane ⊆r EuclideanPlaneStructure
Proof
Definitions occuring in Statement :
euclidean-plane: EuclideanPlane,
euclidean-plane-structure: EuclideanPlaneStructure,
subtype_rel: A ⊆r B
Definitions unfolded in proof :
euclidean-plane: EuclideanPlane,
member: t ∈ T,
subtype_rel: A ⊆r B
Lemmas referenced :
euclidean-plane_wf
Rules used in proof :
hypothesis,
extract_by_obid,
introduction,
cut,
hypothesisEquality,
rename,
thin,
setElimination,
sqequalHypSubstitution,
lambdaEquality,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
EuclideanPlane \msubseteq{}r EuclideanPlaneStructure
Date html generated:
2018_05_22-AM-11_53_00
Last ObjectModification:
2018_05_21-AM-01_13_06
Theory : euclidean!plane!geometry
Home
Index