iSup_eq — Mathlib

English

If x0 is in s and f attains its maximum at x0 on s, then the supremum over s of f equals f(x0).

Русский

Если x0 ∈ s и f достигает максимума на s в x0, то супремум по s функции f равен f(x0).

LaTeX

$$$\\{\\text{hx0}: x_0 \\in s,\\ \\text{h}: \\mathrm{IsMaxOn}(f,s,x_0)\\} \\Rightarrow \\sup_{x\\in s} f(x) = f(x_0)$$$

Lean4

theorem iSup_eq (hx₀ : x₀ ∈ s) (h : IsMaxOn f s x₀) : ⨆ x : s, f x = f x₀ :=
  haveI : Nonempty s := ⟨⟨x₀, hx₀⟩⟩
  ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun x => h x.2) fun _w hw => ⟨⟨x₀, hx₀⟩, hw⟩

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