l_ciSup — Mathlib

English

In a Galois connection, for a bounded-below image of a set s under f, equality l (iSup over s) = iSup over s of l(f i) holds.

Русский

В сопряжении Гали справедливо равенство l( iSup над s ) = iSup над s of l( f(i) ).

LaTeX

$$$ l(\iSup_{i: s} f(i)) = \iSup_{i: s} l(f(i)) $$$

Lean4

theorem l_ciSup (gc : GaloisConnection l u) {f : ι → α} (hf : BddAbove (range f)) : l (⨆ i, f i) = ⨆ i, l (f i) := by
  rw [iSup, gc.l_csSup (range_nonempty _) hf, iSup_range']

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