---

Step * of Lemma mk-s-group_wf

∀[ss:SeparationSpace]. ∀[e:Point]. ∀[i:Point ⟶ Point]. ∀[o:{f:Point ⟶ Point ⟶ Point| 
                                                             (∀x,y,z:Point.  f x (f y z) ≡ f (f x y) z)
                                                             ∧ (∀x:Point. f x e ≡ x)
                                                             ∧ (∀x:Point. f x (i x) ≡ e)} ]. ∀[sep:∀x,x',y,y':Point.
                                                                                                    (o x y # o x' y
                                                                                                    ⇒ (x # x'
                                                                                                       ∨ y # y'))].
∀[invsep:∀x,y:Point.  (i x # i y ⇒ x # y)].
  (mk-s-group(ss; e; i; o; sep; invsep) ∈ s-Group)
BY
{ (Auto
   THEN (Assert ss ∈ SeparationSpace BY
               Auto)
   THEN (D 1 THENA Auto)
   THEN Unfolds ``mk-s-group s-group`` 0
   THEN RepUR ``ss-point ss-sep`` 0
   THEN RepeatFor 5 ((RecordPlusTypeCD
                      THENL [ Id
                            ; (Reduce 0
                               THEN Try ((RepUR ``ss-eq ss-sep`` 0
                                          THEN Folds ``ss-point ss-sep`` 0
                                          THEN Try (Fold `ss-eq` 0)
                                          THEN Trivial))
                               )]
                     ))) }

1
1. ss : self:"Point":Type
        "#":{s:self."Point" ⟶ self."Point" ⟶ ℙ| ∀x:self."Point". (¬(s x x))} 
        "#symm":∀x,y:self."Point".  ((self."#" x y) ⇒ (self."#" y x)) ⋂ x:Atom ⟶ if x =a "#or"
                                                                                   then ∀x,y,z:self."Point".
                                                                                          ((self."#" x y)
                                                                                          ⇒ ((self."#" x z)
                                                                                             ∨ (self."#" y z)))
                                                                                   else Top
                                                                                   fi 
2. ss ∈ record(x.Top)
3. e : Point
4. i : Point ⟶ Point
5. o : {f:Point ⟶ Point ⟶ Point| 
        (∀x,y,z:Point.  f x (f y z) ≡ f (f x y) z) ∧ (∀x:Point. f x e ≡ x) ∧ (∀x:Point. f x (i x) ≡ e)} 
6. sep : ∀x,x',y,y':Point.  (o x y # o x' y ⇒ (x # x' ∨ y # y'))
7. invsep : ∀x,y:Point.  (i x # i y ⇒ x # y)
8. ss ∈ SeparationSpace
9. ss."Point" ∈ Type
10. ss."#" ∈ {s:ss."Point" ⟶ ss."Point" ⟶ ℙ| ∀x:ss."Point". (¬(s x x))} 
11. ss."#symm" ∈ ∀x,y:ss."Point".  ((ss."#" x y) ⇒ (ss."#" y x))
12. ss."#or" ∈ ∀x,y,z:ss."Point".  ((ss."#" x y) ⇒ ((ss."#" x z) ∨ (ss."#" y z)))
⊢ ss["id" := e]["inv" := i]["op" := o]["opsep" := sep]["invsep" := invsep] ∈ SeparationSpace

---

Latex:

---

Latex:
\mforall{}[ss:SeparationSpace].  \mforall{}[e:Point].  \mforall{}[i:Point  {}\mrightarrow{}  Point].  \mforall{}[o:\{f:Point  {}\mrightarrow{}  Point  {}\mrightarrow{}  Point| 
                                                                                                                          (\mforall{}x,y,z:Point.
                                                                                                                                f  x  (f  y  z)  \mequiv{}  f  (f  x  y)  z)
                                                                                                                          \mwedge{}  (\mforall{}x:Point.  f  x  e  \mequiv{}  x)
                                                                                                                          \mwedge{}  (\mforall{}x:Point.  f  x  (i  x)  \mequiv{}  e)\}  ].
\mforall{}[sep:\mforall{}x,x',y,y':Point.    (o  x  y  \#  o  x'  y  {}\mRightarrow{}  (x  \#  x'  \mvee{}  y  \#  y'))].  \mforall{}[invsep:\mforall{}x,y:Point.
                                                                                                                                                        (i  x  \#  i  y  {}\mRightarrow{}  x  \#  y)].
    (mk-s-group(ss;  e;  i;  o;  sep;  invsep)  \mmember{}  s-Group)


By

---

Latex:
(Auto
  THEN  (Assert  ss  \mmember{}  SeparationSpace  BY
                          Auto)
  THEN  (D  1  THENA  Auto)
  THEN  Unfolds  ``mk-s-group  s-group``  0
  THEN  RepUR  ``ss-point  ss-sep``  0
  THEN  RepeatFor  5  ((RecordPlusTypeCD
                                        THENL  [  Id
                                                    ;  (Reduce  0
                                                          THEN  Try  ((RepUR  ``ss-eq  ss-sep``  0
                                                                                THEN  Folds  ``ss-point  ss-sep``  0
                                                                                THEN  Try  (Fold  `ss-eq`  0)
                                                                                THEN  Trivial))
                                                          )]
                                      )))

---

Home Index