---

Step * 1 of Lemma generated-s-subgroup_wf


1. sg : s-Group
2. P : Point ⟶ ℙ
3. ∀f:Point. (P[f] ⇒ P[f^-1])
⊢ ∃L:Point List. ((∀f∈L.P[f]) ∧ 1 ≡ reduce(λx,y. (x y);1;L))
BY
{ (D 0 With ⌜[]⌝  THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  sg  :  s-Group
2.  P  :  Point  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}f:Point.  (P[f]  {}\mRightarrow{}  P[f\^{}-1])
\mvdash{}  \mexists{}L:Point  List.  ((\mforall{}f\mmember{}L.P[f])  \mwedge{}  1  \mequiv{}  reduce(\mlambda{}x,y.  (x  y);1;L))


By

---

Latex:
(D  0  With  \mkleeneopen{}[]\mkleeneclose{}    THEN  Reduce  0  THEN  Auto)

---

Home Index