u_ciInf — Mathlib

English

In a Galois connection, for s : Set γ and f : γ → β with bounded-below image, u( iInf i ∈ s f i ) = iInf i ∈ s u(f i).

Русский

В сопряжении Гали для множества подмножества s и функции f: γ → β выполняется u(инфинум по i∈s f(i)) = инфимум по i∈s u(f(i)).

LaTeX

$$$ u(\inf_{i:\, s} f(i)) = \inf_{i:\, s} u(f(i)) $$$

Lean4

theorem u_ciInf (gc : GaloisConnection l u) {f : ι → β} (hf : BddBelow (range f)) : u (⨅ i, f i) = ⨅ i, u (f i) :=
  gc.dual.l_ciSup hf

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