fst_sSup — Mathlib

English

Supremum of a set of pairs has its first coordinate equal to the supremum of the set of first coordinates.

Русский

Супремум множества пар имеет первую координату, равную супремуму множества первых координат.

LaTeX

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

Lean4

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

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