---

Step * of Lemma permutation-ss-eq-iff

∀[rv:SeparationSpace]. ∀[f,g,f',g':Point ⟶ Point].  uiff(<f, g> ≡ <f', g'>;(∀x:Point. f x ≡ f' x) ∧ (∀x:Point. g x ≡ g'\000C x))
BY
{ (Intros
   THEN RWO "permutation-ss-eq" 0
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN Try ((D -3 THEN RepUR ``fun-sep`` 0 THEN Auto))
   THEN RepeatFor 2 (D -1)
   THEN OnMaybeHyp 6 (\h. ((InstHyp [⌜a⌝] h⋅ THENM (D -1 THEN Trivial)) THENA Auto))) }

---

Latex:

---

Latex:
\mforall{}[rv:SeparationSpace].  \mforall{}[f,g,f',g':Point  {}\mrightarrow{}  Point].
    uiff(<f,  g>  \mequiv{}  <f',  g'>(\mforall{}x:Point.  f  x  \mequiv{}  f'  x)  \mwedge{}  (\mforall{}x:Point.  g  x  \mequiv{}  g'  x))


By

---

Latex:
(Intros
  THEN  RWO  "permutation-ss-eq"  0
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  Try  ((D  -3  THEN  RepUR  ``fun-sep``  0  THEN  Auto))
  THEN  RepeatFor  2  (D  -1)
  THEN  OnMaybeHyp  6  (\mbackslash{}h.  ((InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  h\mcdot{}  THENM  (D  -1  THEN  Trivial))  THENA  Auto)))

---

Home Index