snd_iSup — Mathlib

English

The second coordinate of the supremum of a family of pairs equals the supremum of the second coordinates: (iSup f).snd = ⨆ i, (f i).snd.

Русский

Вторая координата супремума семейства пар равна супремуму вторых координат: (iSup f).snd = ⨆ i, (f i).snd.

LaTeX

$$$(\mathrm{iSup}\, f).\mathrm{snd} = \bigsup_i (f(i).\mathrm{snd}).$$$

Lean4

theorem snd_iSup [SupSet α] [SupSet β] (f : ι → α × β) : (iSup f).snd = ⨆ i, (f i).snd :=
  congr_arg sSup (range_comp _ _).symm

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