biInf_mem — Mathlib

English

For l HasBasis p s and a monotone f, the infimum over t ∈ l of f t equals the infimum over i of f(s i) for i with p i.

Русский

Для HasBasis l p s и монотонной функции f, инфимум по t ∈ l f(t) равен инфимума по i: f(s(i)) для i, удовлетворяющих p(i).

LaTeX

$$$ \inf_{t \in l} f(t) = \inf_{i} f(s(i)) $$$

Lean4

protected theorem biInf_mem [CompleteLattice β] {f : Set α → β} (h : HasBasis l p s) (hf : Monotone f) :
    ⨅ t ∈ l, f t = ⨅ (i) (_ : p i), f (s i) :=
  le_antisymm (le_iInf₂ fun i hi => iInf₂_le (s i) (h.mem_of_mem hi)) <|
    le_iInf₂ fun _t ht =>
      let ⟨i, hpi, hi⟩ := h.mem_iff.1 ht
      iInf₂_le_of_le i hpi (hf hi)

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