English
Let e be an order isomorphism between ConditionallyCompleteLattices α and β. For any function f from an index set ι to α which is bounded above, e maps the supremum of the f-values to the supremum of the mapped values; i.e., e(⨆i f(i)) = ⨆i e(f(i)).
Русский
Пусть e — биективное отображение упорядоченности между частично упорядоченными непустыми условиями α и β. Для любой функции f : ι → α, ограниченной сверху, сохранение сверху выполняется: e(⨆i f(i)) = ⨆i e(f(i)).
LaTeX
$$$e\\left(\\big\\vee_{i} f(i)\\right) = \\big\\vee_{i} e\\big(f(i)\\big)\\quad \\text{(при условии, что } \\{f(i) : i\\in ι\\}\\text{ над } α \\\\text{ограничено сверху)}$$$
Lean4
theorem map_ciSup (e : α ≃o β) {f : ι → α} (hf : BddAbove (range f)) : e (⨆ i, f i) = ⨆ i, e (f i) :=
e.to_galoisConnection.l_ciSup hf
