klFun_eq_zero_iff — Mathlib

English

For x ≥ 0, klFun(x) = 0 if and only if x = 1.

Русский

Для x ≥ 0, klFun(x) = 0 тогда и только тогда, когда x = 1.

LaTeX

$$$\\mathrm{klFun}(x) = 0 \\iff x = 1 \\quad (x \\ge 0)$$$

Lean4

theorem klFun_eq_zero_iff (hx : 0 ≤ x) : klFun x = 0 ↔ x = 1 :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ by simp [klFun_apply, h]⟩
  exact
    strictConvexOn_klFun.eq_of_isMinOn (isMinOn_iff.mpr fun y hy ↦ h ▸ klFun_nonneg hy) isMinOn_klFun hx
      (zero_le_one' ℝ)

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