inf'_id_eq_csInf — Mathlib

English

If ι is finite and nonempty, then the supremum over the universe equals the iSup over all i.

Русский

Если множество индексов ι конечное и непустое, то верхняя граница по всем i равна iSup по всем i.

LaTeX

$$$\mathrm{univ}.sup'\; \mathrm{univ\_nonempty}\ f = \bigvee_{i} f(i)$$$

Lean4

theorem inf'_id_eq_csInf (s : Finset α) (hs) : s.inf' hs id = sInf s :=
  sup'_id_eq_csSup (α := αᵒᵈ) _ hs

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