uniqueDiffWithinAt_Ici — Mathlib

English

For every x ∈ ℝ, the closed ray Ici(x) = [x, ∞) is a set of unique differentiability at the point x.

Русский

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

LaTeX

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

Lean4

theorem uniqueDiffWithinAt_Ici (x : ℝ) : UniqueDiffWithinAt ℝ (Ici x) x :=
  (uniqueDiffWithinAt_Ioi x).mono Set.Ioi_subset_Ici_self

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