snd_sInf — Mathlib

English

For S ⊆ α×β with SupSet, the first coordinate of the supremum equals the supremum of the set of first coordinates.

Русский

Для множества S ⊆ α×β с SupSet, первая координата супремума равна супремуму множества первых координат элементов S.

LaTeX

$$$\mathrm{fst}(\mathrm{sSup}\, S) = \mathrm{sSup}(\mathrm{fst}'' S)$$$

Lean4

theorem snd_sInf [InfSet α] [InfSet β] (s : Set (α × β)) : (sInf s).snd = sInf (Prod.snd '' s) :=
  rfl

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