Nuprl Lemma : euclidean-plane-structure-subtype
EuclideanPlaneStructure ⊆r GeometryPrimitives
Proof
Definitions occuring in Statement :
euclidean-plane-structure: EuclideanPlaneStructure,
geo-primitives: GeometryPrimitives,
subtype_rel: A ⊆r B
Definitions unfolded in proof :
record+: record+,
euclidean-plane-structure: EuclideanPlaneStructure,
member: t ∈ T,
subtype_rel: A ⊆r B
Lemmas referenced :
euclidean-plane-structure_wf
Rules used in proof :
extract_by_obid,
introduction,
cut,
universeIsType,
equalitySymmetry,
hypothesis,
equalityTransitivity,
dependentIntersectionEqElimination,
sqequalRule,
thin,
dependentIntersectionElimination,
sqequalHypSubstitution,
lambdaEquality_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
EuclideanPlaneStructure \msubseteq{}r GeometryPrimitives
Date html generated:
2019_10_29-AM-09_13_06
Last ObjectModification:
2019_10_25-PM-02_06_25
Theory : euclidean!plane!geometry
Home
Index