iInf_eq_iInf_subseq_of_monotone — Mathlib

English

Let ι1, ι2, α be types with ι2 preordered and α a complete lattice. For a Filter l on ι1 with l.NeBot, a monotone f: ι2 → α and Tendsto φ l atBot, then iInf f = iInf (f ∘ φ).

Русский

Пусть ι1, ι2, α — типы, ι2 упорядочен, α — полная решетка. Для фильтра l на ι1 с l.NeBot, монотонная f: ι2 → α и Tendsto φ l atBot, тогда infimum f(i) по i равно infimum f(φ(i)).

LaTeX

$$$\text{Monotone}(f) \Rightarrow \operatorname{Infimum}_{i} f(i) = \operatorname{Infimum}_{i} f(\phi(i))$$$

Lean4

theorem iInf_eq_iInf_subseq_of_monotone {ι₁ ι₂ α : Type*} [Preorder ι₂] [CompleteLattice α] {l : Filter ι₁} [l.NeBot]
    {f : ι₂ → α} {φ : ι₁ → ι₂} (hf : Monotone f) (hφ : Tendsto φ l atBot) : ⨅ i, f i = ⨅ i, f (φ i) :=
  iSup_eq_iSup_subseq_of_monotone hf.dual hφ

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