map_iSup — Mathlib

English

Let f be an order isomorphism between complete lattices α and β. Then for any family x: ι → α, f(⨆ i, x(i)) = ⨆ i, f(x(i)).

Русский

Пусть f — обратимое по порядку отображение между полными решетками α и β. Тогда для любой семейства x: ι → α выполняется равенство f( sup_i x(i) ) = sup_i f(x(i)).

LaTeX

$$$f\\\\left(\\\\big\\\\vee_{i} x_i\\\\right) = \\\\big\\\\vee_{i} f(x_i)$$$

Lean4

theorem map_iSup [CompleteLattice β] (f : α ≃o β) (x : ι → α) : f (⨆ i, x i) = ⨆ i, f (x i) :=
  eq_of_forall_ge_iff <| f.surjective.forall.2 fun x => by simp only [f.le_iff_le, iSup_le_iff]

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