iInf_eq — Mathlib

English

If x0 is in s and f attains its minimum at x0 on s, then the infimum 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{IsMinOn}(f,s,x_0)\\} \\Rightarrow \\inf_{x\\in s} f(x) = f(x_0)$$$

Lean4

theorem iInf_eq (hx₀ : x₀ ∈ s) (h : IsMinOn f s x₀) : ⨅ x : s, f x = f x₀ :=
  @IsMaxOn.iSup_eq αᵒᵈ β _ _ _ _ hx₀ h

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