not_sameRay_iff_of_norm_eq

Mathlib.Analysis.Normed.Module.Ray

URI: https://scilib.ai/kg/mathlib#not_sameRay_iff_of_norm_eq

English

If ‖x‖ = ‖y‖, then not SameRay x y is equivalent to x ≠ y.

Русский

Если ‖x‖ = ‖y‖, то неравенство луча не совпадает с условиями, и наоборот, x ≠ y.

LaTeX

$$$$ \|x\| = \|y\| \Rightarrow (\lnot \text{SameRay}(x,y)) \iff x \neq y. $$$$

Lean4

theorem not_sameRay_iff_of_norm_eq (h : ‖x‖ = ‖y‖) : ¬SameRay ℝ x y ↔ x ≠ y :=
  (sameRay_iff_of_norm_eq h).not

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru