iInf_eq_iInf_subseq_of_antitone — Mathlib

English

Let ι1, ι2, α be types with ι2 preordered and α a complete lattice. For an Antitone f: ι2 → α and Tendsto φ l atTop, iInf f = iInf (f ∘ φ).

Русский

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

LaTeX

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

Lean4

theorem iInf_eq_iInf_subseq_of_antitone {ι₁ ι₂ α : Type*} [Preorder ι₂] [CompleteLattice α] {l : Filter ι₁} [l.NeBot]
    {f : ι₂ → α} {φ : ι₁ → ι₂} (hf : Antitone f) (hφ : Tendsto φ l atTop) : ⨅ i, f i = ⨅ i, f (φ i) :=
  iSup_eq_iSup_subseq_of_antitone hf.dual hφ

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