---

Step * of Lemma rv-isometry-implies-functional

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

1
1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. Isometry(f)
4. x : Point
5. y : Point
6. f x # f y ⇒ x # y
⊢ x ≡ y ⇒ f x ≡ f y

---

Latex:

---

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


By

---

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

---

Home Index