direction_sup_eq_sup_direction — Mathlib

English

If the two affine subspaces share a point, the direction of their supremum equals the supremum of their directions.

Русский

Если две подпространства имеют общую точку, направление их супремума равно объединению их направлений.

LaTeX

$$$ (s_1 \\sqcup s_2).\\mathrm{direction} = s_1.\\mathrm{direction} \\sqcup s_2.\\mathrm{direction} $$$

Lean4

/-- The direction of the sup of two affine subspaces with a common point is the sup of the two
directions. -/
theorem direction_sup_eq_sup_direction {s₁ s₂ : AffineSubspace k P} {p : P} (hp₁ : p ∈ s₁) (hp₂ : p ∈ s₂) :
    (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction :=
  by
  rw [direction_sup hp₁ hp₂]
  simp

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