English
Let α and β be types with a supremum structure on sets, and let f be a function from an index set ι to α × β. Then swapping coordinates commutes with taking the supremum: the swap of the supremum equals the supremum of the swapped coordinates, i.e. (iSup f).swap = ⨆ i, (f i).swap.
Русский
Пусть α и β — множества с структурой верхней грани над подмножествами, и имеется отображение f : ι → α × β. Тогда разворот координат коммутирует с взятиемsupremum:.swap верхней грани (iSup f) равен верхней грани множества { (f i).swap : i ∈ ι }.
LaTeX
$$$ (iSup f).swap = ⨆ i, (f i).swap $$$
Lean4
theorem swap_iSup [SupSet α] [SupSet β] (f : ι → α × β) : (iSup f).swap = ⨆ i, (f i).swap := by
simp_rw [iSup, swap_sSup, ← range_comp, comp_def]
