map_ciSup_set — Mathlib

English

Let e be an order isomorphism between α and β. For a nonempty set s and a function f: s → α whose image is bounded above, we have e(⨆ i: s, f i) = ⨆ i: s, e(f i).

Русский

Пусть e — упорядочивающее отображение между α и β. Пусть s непустоe множество и f: s → α таково, что образ f ограничен сверху. Тогда e(⨆i∈s f(i)) = ⨆i∈s e(f(i)).

LaTeX

$$$e\\left(\\bigvee_{i\\in s} f(i)\\right) = \\bigvee_{i\\in s} e\\left(f(i)\\right)$$$

Lean4

theorem map_ciSup_set (e : α ≃o β) {s : Set γ} {f : γ → α} (hf : BddAbove (f '' s)) (hne : s.Nonempty) :
    e (⨆ i : s, f i) = ⨆ i : s, e (f i) :=
  e.to_galoisConnection.l_ciSup_set hf hne

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