uniqueDiffWithinAt_Ioo — Mathlib

English

For any a, b ∈ ℝ and any t with t ∈ Ioo(a,b), the point t is a unique differentiability point within the set Ioo(a,b).

Русский

Для любых a,b ∈ ℝ и t, принадлежащего Ioo(a,b), точка t является точкой уникальной дифференцируемости внутри множества Ioo(a,b).

LaTeX

$$$\forall a,b,t\in\mathbb{R},\ t\in\mathrm{Ioo}(a,b)\ \Rightarrow\ \mathrm{UniqueDiffWithinAt}_{\mathbb{R}}(\mathrm{Ioo}(a,b))\,t$$$

Lean4

theorem uniqueDiffWithinAt_Ioo {a b t : ℝ} (ht : t ∈ Set.Ioo a b) : UniqueDiffWithinAt ℝ (Set.Ioo a b) t :=
  IsOpen.uniqueDiffWithinAt isOpen_Ioo ht

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