l_ciSup_set — Mathlib

English

Let gc be a Galois connection; for any nonempty s ⊆ β with BddBelow, u(sInf s) = iInf x∈s u(x).

Русский

Пусть gc — сопряжение Гали; для не пустого s ⊆ β с нижней ограниченностью выполняется u(inf s) = inf { u(x) : x ∈ s }.

LaTeX

$$$ u(\mathrm{sInf} s) = \inf_{x \in s} u(x) $$$

Lean4

theorem l_ciSup_set (gc : GaloisConnection l u) {s : Set γ} {f : γ → α} (hf : BddAbove (f '' s)) (hne : s.Nonempty) :
    l (⨆ i : s, f i) = ⨆ i : s, l (f i) := by
  haveI := hne.to_subtype
  rw [image_eq_range] at hf
  exact gc.l_ciSup hf

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