swap_sSup — Mathlib

English

Swapping the coordinates commutes with supremum: the supremum of the swapped set is the swap of the supremum.

Русский

Замена координат сохраняет супремум: супремум замещённого множества равен замещённому супремуму исходного множества.

LaTeX

$$$\mathrm{swap}(\mathrm{sSup}\, s) = \mathrm{sSup}(\mathrm{Prod.swap}'' s)$$$

Lean4

theorem swap_sSup [SupSet α] [SupSet β] (s : Set (α × β)) : (sSup s).swap = sSup (Prod.swap '' s) :=
  Prod.ext (congr_arg sSup <| image_comp Prod.fst swap s) (congr_arg sSup <| image_comp Prod.snd swap s)

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