---

Step * of Lemma separable-translation-group_iff

No Annotations
∀rv:InnerProductSpace. ∀e:{e:Point(rv)| e^2 = r1} . ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
  (translation-group-fun(rv;e;T)
  ⇒ (separable-translation-group(rv;e;T)
     ⇐⇒ (∀a:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .  (a ≠ r0 ⇒ (r0 < ||T_a(h) - h||)))
         ∧ (∀a,b:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .
              (a ≠ r0 ⇒ b ≠ r0 ⇒ ((||T_a(h) - h||/||T_b(h) - h||) = (||T_a(0)||/||T_b(0)||))))))
BY
{ (RepeatFor 4 ((Intro THENA Auto)) THEN (RepeatFor 2 (D 0) THENW Auto)) }

1
1. rv : InnerProductSpace
2. e : {e:Point(rv)| e^2 = r1} 
3. T : ℝ ⟶ Point(rv) ⟶ Point(rv)
4. translation-group-fun(rv;e;T)
5. separable-translation-group(rv;e;T)
⊢ (∀a:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .  (a ≠ r0 ⇒ (r0 < ||T_a(h) - h||)))
∧ (∀a,b:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .
     (a ≠ r0 ⇒ b ≠ r0 ⇒ ((||T_a(h) - h||/||T_b(h) - h||) = (||T_a(0)||/||T_b(0)||))))

2
1. rv : InnerProductSpace
2. e : {e:Point(rv)| e^2 = r1} 
3. T : ℝ ⟶ Point(rv) ⟶ Point(rv)
4. translation-group-fun(rv;e;T)
5. (∀a:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .  (a ≠ r0 ⇒ (r0 < ||T_a(h) - h||)))
∧ (∀a,b:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .
     (a ≠ r0 ⇒ b ≠ r0 ⇒ ((||T_a(h) - h||/||T_b(h) - h||) = (||T_a(0)||/||T_b(0)||))))
⊢ separable-translation-group(rv;e;T)

3
1. rv : InnerProductSpace
2. e : {e:Point(rv)| e^2 = r1} 
3. T : ℝ ⟶ Point(rv) ⟶ Point(rv)
4. translation-group-fun(rv;e;T)
5. x : ∀a:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .  (a ≠ r0 ⇒ (r0 < ||T_a(h) - h||))
6. a : ℝ
7. b : ℝ
8. h : {h:Point(rv)| h ⋅ e = r0} 
9. x1 : a ≠ r0
10. x2 : b ≠ r0
⊢ ||T_b(0)|| ≠ r0

---

Latex:

---

Latex:
No  Annotations
\mforall{}rv:InnerProductSpace.  \mforall{}e:\{e:Point(rv)|  e\^{}2  =  r1\}  .  \mforall{}T:\mBbbR{}  {}\mrightarrow{}  Point(rv)  {}\mrightarrow{}  Point(rv).
    (translation-group-fun(rv;e;T)
    {}\mRightarrow{}  (separable-translation-group(rv;e;T)
          \mLeftarrow{}{}\mRightarrow{}  (\mforall{}a:\mBbbR{}.  \mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .    (a  \mneq{}  r0  {}\mRightarrow{}  (r0  <  ||T\_a(h)  -  h||)))
                  \mwedge{}  (\mforall{}a,b:\mBbbR{}.  \mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .
                            (a  \mneq{}  r0  {}\mRightarrow{}  b  \mneq{}  r0  {}\mRightarrow{}  ((||T\_a(h)  -  h||/||T\_b(h)  -  h||)  =  (||T\_a(0)||/||T\_b(0)||))))))


By

---

Latex:
(RepeatFor  4  ((Intro  THENA  Auto))  THEN  (RepeatFor  2  (D  0)  THENW  Auto))

---

Home Index