English
Let f be an order isomorphism between complete lattices α and β. For a family x(i) with index i and j, f(⨆ i, ⨆ j, x(i,j)) = ⨆ i, ⨆ j, f(x(i,j)).
Русский
Пусть f — порядок-изоморфизм между полными решетками α и β. Тогда для двухпорядкового массива x(i,j) выполняется f(верхний предел по i и j) = верхний предел по i и j от f(x(i,j)).
LaTeX
$$$f\\\\left(\\\\big\\\\vee_{i}\\\\big\\\\vee_{j} x(i,j)\\\\right) = \\\\big\\\\vee_{i}\\\\big\\\\vee_{j} f(x(i,j))$$$
Lean4
theorem map_iSup₂ [CompleteLattice β] (f : α ≃o β) (x : ∀ i, κ i → α) : f (⨆ i, ⨆ j, x i j) = ⨆ i, ⨆ j, f (x i j) :=
eq_of_forall_ge_iff <| f.surjective.forall.2 fun x => by simp only [f.le_iff_le, iSup_le_iff]
