u_csInf' — Mathlib

English

Let gc be a Galois connection; for any nonempty ι and f : ι → β with BddBelow, u(iInf f) = iInf (λ x, u(f x)).

Русский

Пусть gc — сопряжение Гали; для непустого ι и f : ι → β с нижней ограниченностью имеем u(иInf f) = inf { u(f(i)) : i ∈ ι }.

LaTeX

$$$ u(\inf_{i} f(i)) = \inf_{i} u(f(i)) $$$

Lean4

theorem u_csInf' (gc : GaloisConnection l u) {s : Set β} (hne : s.Nonempty) (hbdd : BddBelow s) :
    u (sInf s) = sInf (u '' s) :=
  gc.dual.l_csSup' hne hbdd

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