---

Step * of Lemma rv-orthogonal-implies-extensional

∀rv:InnerProductSpace. ∀f:Point ⟶ Point.  ∀x,y:Point.  (f x # f y ⇒ x # y) supposing Orthogonal(f)
BY
{ (InstLemma `rv-isometry-implies-extensional` []
   THEN (RepeatFor 3 (ParallelLast') THENA Auto)
   THEN InstLemma `rv-orthogonal-isometry` [⌜rv⌝;⌜f⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}f:Point  {}\mrightarrow{}  Point.    \mforall{}x,y:Point.    (f  x  \#  f  y  {}\mRightarrow{}  x  \#  y)  supposing  Orthogonal(f)


By

---

Latex:
(InstLemma  `rv-isometry-implies-extensional`  []
  THEN  (RepeatFor  3  (ParallelLast')  THENA  Auto)
  THEN  InstLemma  `rv-orthogonal-isometry`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index