---

Step * of Lemma rv-orthogonal-implies-functional

∀[rv:InnerProductSpace]. ∀f:Point ⟶ Point. (Orthogonal(f) ⇒ (∀x,y:Point.  (x ≡ y ⇒ f x ≡ f y)))
BY
{ (InstLemma `rv-isometry-implies-functional` [] THEN (RepeatFor 3 (ParallelLast') THENA Auto)) }

1
.....antecedent..... 
1. [rv] : InnerProductSpace
2. f : Point ⟶ Point
3. Orthogonal(f)
⊢ Isometry(f)

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}f:Point  {}\mrightarrow{}  Point.  (Orthogonal(f)  {}\mRightarrow{}  (\mforall{}x,y:Point.    (x  \mequiv{}  y  {}\mRightarrow{}  f  x  \mequiv{}  f  y)))


By

---

Latex:
(InstLemma  `rv-isometry-implies-functional`  []  THEN  (RepeatFor  3  (ParallelLast')  THENA  Auto))

---

Home Index