of_subsingleton

Mathlib.LinearAlgebra.Ray

URI: https://scilib.ai/kg/mathlib#SameRay.of_subsingleton

English

If the ambient module is a subsingleton, then any two vectors lie on the same ray.

Русский

Если модуль — подсинглтон, то любые два вектора лежат на одном луче.

LaTeX

$$$[Subsingleton M] \\Rightarrow \\forall x,y\\,\\; SameRay R x y$$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton M] (x y : M) : SameRay R x y :=
  by
  rw [Subsingleton.elim x 0]
  exact zero_left _

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

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

Разделы

Аффилиация

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