uniqueDiffWithinAt_Iio — Mathlib

English

For every a ∈ ℝ, the open ray Iio(a) = (−∞, a) has the unique differentiability property at its right endpoint a.

Русский

Для каждого a ∈ ℝ луч Iio(a) = (−∞, a) обладает уникальной дифференцируемостью в точке a.

LaTeX

$$$\forall a\in\mathbb{R},\, \mathrm{UniqueDiffWithinAt}_{\mathbb{R}}(\mathrm{Iio}(a))\,a$$$

Lean4

theorem uniqueDiffWithinAt_Iio (a : ℝ) : UniqueDiffWithinAt ℝ (Iio a) a :=
  uniqueDiffWithinAt_convex (convex_Iio a) (by simp) (by simp)

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