fst_sInf — Mathlib

English

For S ⊆ α×β with InfSet structure, the first coordinate of the infimum equals the infimum of the set of first coordinates.

Русский

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

LaTeX

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

Lean4

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

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