map_csSup — Mathlib

English

Let gc be a Galois connection; for s : Set γ and f : γ → α with BddAbove (f '' s), and s nonempty, l( iSup i:s f i ) = iSup i:s, l(f i).

Русский

Пусть gc — сопряжение Гали; для множества s и отображения f с ограниченной сверху image, не пустого s выполняется l( iSup_{i∈s} f(i) ) = iSup_{i∈s} l(f(i)).

LaTeX

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

Lean4

theorem map_csSup (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) : e (sSup s) = ⨆ x : s, e x :=
  e.to_galoisConnection.l_csSup hne hbdd

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