uniqueDiffWithinAt_Iic — Mathlib

English

For every x ∈ ℝ, the closed ray Iic(x) = (−∞, x] has the unique differentiability property at x.

Русский

Для любой точки x на ℝ луч Iic(x) = (−∞, x] имеет уникальную дифференцируемость в точке x.

LaTeX

$$$\forall x\in\mathbb{R},\ \mathrm{UniqueDiffWithinAt}_{\mathbb{R}}(\mathrm{Iic}(x))\,x$$$

Lean4

theorem uniqueDiffWithinAt_Iic (x : ℝ) : UniqueDiffWithinAt ℝ (Iic x) x :=
  (uniqueDiffWithinAt_Iio x).mono Set.Iio_subset_Iic_self

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