uniqueDiffWithinAt_Ioi — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem uniqueDiffWithinAt_Ioi (a : ℝ) : UniqueDiffWithinAt ℝ (Ioi a) a :=
  uniqueDiffWithinAt_convex (convex_Ioi a) (by simp) (by simp)

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