English
Let α be nonempty and D: α → β with β a semilattice with supremum. If b belongs to the range of D, the preimage of b lies in s, and b is an upper bound of { D(a) : a ∈ s }, then the supremum of D over s equals b.
Русский
Пусть α непусто, D: α → β, β — полуполе с верхней гранью. Если b принадлежит образу D и D^{-1}(b) ∈ s и b является верхней границей множества { D(a) : a ∈ s }, тогда s.sup D = b.
LaTeX
$$$b \\in \\mathrm{range}(D) \\ \\,\\land \\, D^{-1}(b) \\in s \\\\land \\, \\forall a \\in s,\\ D(a) \\le b \\Rightarrow s.sup D = b$$$
Lean4
theorem sup_eq_of_max [Nonempty α] {b : β} (hb : b ∈ Set.range D) (hmem : D.invFun b ∈ s) (hmax : ∀ a ∈ s, D a ≤ b) :
s.sup D = b := by
obtain ⟨a, rfl⟩ := hb
rw [← Function.apply_invFun_apply (f := D)]
apply sup_eq_of_isMaxOn hmem; intro
rw [Function.apply_invFun_apply (f := D)]; apply hmax
