direction_sInf — Mathlib

English

The direction of the infimum is bounded above by the infimum of directions.

Русский

Направление наименьшего элемента ограничено сверху пересечением направлений.

LaTeX

$$direction (sInf t) ≤ ⨅ s ∈ t, s.direction$$

Lean4

theorem direction_sInf (t : Set (AffineSubspace k P)) : direction (sInf t) ≤ ⨅ s ∈ t, s.direction :=
  by
  simp only [direction_eq_vectorSpan, vectorSpan_def]
  exact le_iInf₂ fun s hs => Submodule.span_mono <| vsub_self_mono <| biInter_subset_of_mem hs

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