swap_sInf — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem swap_sInf [InfSet α] [InfSet β] (s : Set (α × β)) : (sInf s).swap = sInf (Prod.swap '' s) :=
  Prod.ext (congr_arg sInf <| image_comp Prod.fst swap s) (congr_arg sInf <| image_comp Prod.snd swap s)

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