map_ciInf_set — Mathlib

English

For an order isomorphism e and a nonempty s with f: s→α such that f''s is bounded below, e(sInf s) = sInf (e''s).

Русский

При существовании отображения e и непустого множества s с функцией f: s→α, ограниченного снизу, выполняется e(sInf s) = sInf (e''s).

LaTeX

$$$e\\left( sInf\, s \\right) = sInf\\left( e''s \\right)$$$

Lean4

theorem map_ciInf_set (e : α ≃o β) {s : Set γ} {f : γ → α} (hf : BddBelow (f '' s)) (hne : s.Nonempty) :
    e (⨅ i : s, f i) = ⨅ i : s, e (f i) :=
  e.dual.map_ciSup_set hf hne

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