direction_eq

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

URI: https://scilib.ai/kg/mathlib#AffineSubspace.Parallel.direction_eq

English

If s1 ∥ s2, then their directions are equal: s1.direction = s2.direction.

Русский

Если s1 параллельно s2, то их направления равны: s1.direction = s2.direction.

LaTeX

$$$ s_1 \\parallel s_2 \\Rightarrow s_1.\\mathrm{direction} = s_2.\\mathrm{direction} $$$

Lean4

theorem direction_eq {s₁ s₂ : AffineSubspace k P} (h : s₁ ∥ s₂) : s₁.direction = s₂.direction :=
  by
  rcases h with ⟨v, rfl⟩
  simp

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

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

Разделы

Аффилиация

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