sup_direction_le — Mathlib

English

The direction of the supremum of two affine subspaces contains the supremum of their directions.

Русский

Направление наибольшего из двух аффинных подпрообразований содержит наибольшее их направлений.

LaTeX

$$$\mathrm{dir}(s_1) \;\sqcup\; \mathrm{dir}(s_2) \le \mathrm{dir}(s_1 \sqcup s_2).$$$

Lean4

/-- The sup of the directions of two affine subspaces is less than or equal to the direction of
their sup. -/
theorem sup_direction_le (s₁ s₂ : AffineSubspace k P) : s₁.direction ⊔ s₂.direction ≤ (s₁ ⊔ s₂).direction :=
  by
  simp only [direction_eq_vectorSpan, vectorSpan_def]
  exact
    sup_le (sInf_le_sInf fun p hp => Set.Subset.trans (vsub_self_mono (le_sup_left : s₁ ≤ s₁ ⊔ s₂)) hp)
      (sInf_le_sInf fun p hp => Set.Subset.trans (vsub_self_mono (le_sup_right : s₂ ≤ s₁ ⊔ s₂)) hp)

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