snd_sSup — Mathlib

English

The second coordinate of the supremum of a set of pairs equals the supremum of the set of second coordinates.

Русский

Вторая координата супремума множества пар равна супремуму множества вторых координат.

LaTeX

$$$\mathrm{snd}(\mathrm{sSup}\, s) = \mathrm{sSup}(\mathrm{snd}'' s)$$$

Lean4

theorem snd_sSup [SupSet α] [SupSet β] (s : Set (α × β)) : (sSup s).snd = sSup (Prod.snd '' s) :=
  rfl

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