Step
*
of Lemma
euclidean-structure_wf
EuclideanStructure ∈ 𝕌'
BY
{ (Unfold `euclidean-structure` 0 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