empty

Mathlib.Analysis.Calculus.FDeriv.Basic

URI: https://scilib.ai/kg/mathlib#DifferentiableWithinAt.empty

English

DifferentiableWithinAt 𝕜 f ∅ x holds trivially for any f and x.

Русский

Дифференцируемость внутри пустого множества тождественно истинна для любой f и x.

LaTeX

$$$$\\text{DifferentiableWithinAt } 𝕜 f \\emptyset x.$$$$

Lean4

@[simp]
protected theorem empty : DifferentiableWithinAt 𝕜 f ∅ x :=
  ⟨0, .empty⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru