direction_sInf_of_mem — Mathlib

English

The direction of the infimum over a family is bounded above by the infimum of the individual directions.

Русский

Направление iInf семейства подпро пространств ограничено сверху инфимом отдельных направлений.

LaTeX

$$direction (iInf s) ≤ ⨅ i, (s i).direction$$

Lean4

theorem direction_sInf_of_mem (t : Set (AffineSubspace k P)) (p : P) (h : ∀ s ∈ t, p ∈ s) :
    direction (sInf t) = ⨅ s ∈ t, s.direction :=
  by
  apply (direction_sInf t).antisymm
  intro v hv
  rw [← vadd_mem_iff_mem_direction v ((mem_sInf_iff p t).mpr h), mem_sInf_iff]
  intro s hs
  rw [vadd_mem_iff_mem_direction v (h s hs)]
  simp only [Submodule.mem_iInf] at hv
  exact hv s hs

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