uniqueDiffOn_Ico — 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, множество пусто и поэтому trivially имеет это свойство.

LaTeX

$$$ (a

Lean4

theorem uniqueDiffOn_Ico (a b : ℝ) : UniqueDiffOn ℝ (Ico a b) :=
  if hab : a < b then uniqueDiffOn_convex (convex_Ico a b) <| by simp only [interior_Ico, nonempty_Ioo, hab]
  else by simp only [Ico_eq_empty hab, uniqueDiffOn_empty]

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