fst_iSup — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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