uniqueDiffOn_Ioc — Mathlib

English

For real a < b, the half-open interval (a,b] has UniqueDiffOn; if a ≥ b, the set is empty and trivially has UniqueDiffOn.

Русский

Для a < b полублоковый интервал (a,b] имеет уникальную дифференцируемость; если a ≥ b, множество пусто и поэтому тривиально имеет это свойство.

LaTeX

$$$ (a

Lean4

theorem uniqueDiffOn_Ioc (a b : ℝ) : UniqueDiffOn ℝ (Ioc a b) :=
  if hab : a < b then uniqueDiffOn_convex (convex_Ioc a b) <| by simp only [interior_Ioc, nonempty_Ioo, hab]
  else by simp only [Ioc_eq_empty hab, uniqueDiffOn_empty]

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