English
Let s be a finite subset of α and D: α → β, where β is a semi-lattice with a supremum. If a ∈ s and D(a) is the maximum of { D(x) | x ∈ s }, then the supremum of D over s equals D(a).
Русский
Пусть s — конечное множество индексов в α и D: α → β, где β обладает наибольшей верхней гранью. Если a ∈ s и D(a) является максимумом значений { D(x) | x ∈ s }, то sup_{x∈s} D(x) = D(a).
LaTeX
$$$\\Big( a \\in s \\Big) \\wedge \\Big( \\text{IsMaxOn } D\\ s\ even a \\Rightarrow \\sup_{x \\in s} D(x) = D(a) \\Big$$$
Lean4
theorem sup_eq_of_isMaxOn {a : α} (hmem : a ∈ s) (hmax : IsMaxOn D s a) : s.sup D = D a :=
(Finset.sup_le hmax).antisymm (Finset.le_sup hmem)
