hasLineDerivWithinAt_univ — Mathlib

English

The universal case for line derivatives: HasLineDerivWithinAt with univ is equivalent to HasLineDerivAt.

Русский

Единичный случай для линейной производной: HasLineDerivWithinAt на Set.univ эквивалентна HasLineDerivAt.

LaTeX

$$$HasLineDerivWithinAt 𝕜 f f' univ x v \iff HasLineDerivAt 𝕜 f f' x v.$$$

Lean4

@[simp]
theorem hasLineDerivWithinAt_univ : HasLineDerivWithinAt 𝕜 f f' univ x v ↔ HasLineDerivAt 𝕜 f f' x v := by
  simp only [HasLineDerivWithinAt, HasLineDerivAt, preimage_univ, hasDerivWithinAt_univ]

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