Step * of Lemma euclidean-structure_wf

EuclideanStructure ∈ 𝕌'
BY
(Unfold `euclidean-structure` THEN RecordWf THEN Try (Complete (Auto))) }


Latex:


Latex:
EuclideanStructure  \mmember{}  \mBbbU{}'


By


Latex:
(Unfold  `euclidean-structure`  0  THEN  RecordWf  THEN  Try  (Complete  (Auto)))




Home Index