sup_const — Mathlib

English

Let α be a semilattice with bottom. If s is a nonempty finite set of β and c ∈ α, then the supremum over s of the constant value c equals c.

Русский

Пусть α — полупорядоченное множество с единицей (ниже) и s — непустое конечное множество элементов β; для любого c ∈ α супремум по s константы c равен c.

LaTeX

$$$\displaystyle \forall c \in \alpha,\quad \sup_{x\in s} c = c$$$

Lean4

theorem sup_const {s : Finset β} (h : s.Nonempty) (c : α) : (s.sup fun _ => c) = c :=
  eq_of_forall_ge_iff (fun _ => Finset.sup_le_iff.trans h.forall_const)

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