direction_inf — Mathlib

English

The underlying set of the infimum equals the intersection of the member sets.

Русский

Основанное множество наименьшего элемента равняется пересечению множеств участников.

LaTeX

$$$(sInf t : AffineSubspace k P) : Set P = \bigcap_{s \in t} (s : Set P)$$$

Lean4

/-- The direction of the inf of two affine subspaces is less than or equal to the inf of their
directions. -/
theorem direction_inf (s₁ s₂ : AffineSubspace k P) : (s₁ ⊓ s₂).direction ≤ s₁.direction ⊓ s₂.direction :=
  by
  simp only [direction_eq_vectorSpan, vectorSpan_def]
  exact
    le_inf (sInf_le_sInf fun p hp => trans (vsub_self_mono inter_subset_left) hp)
      (sInf_le_sInf fun p hp => trans (vsub_self_mono inter_subset_right) hp)

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