of_notMem_closure — Mathlib

English

If the base point x lies outside the closure of s, then f has any derivative within s at x; this is a vacuous truth since there is no approach within s to x.

Русский

Если точка x лежит вне замыкания s, то f имеет любую производную внутри s в точке x; это тавтология, поскольку к x нельзя приблизиться внутри s.

LaTeX

$$$\bigl(x \notin \overline{s}\bigr) \Rightarrow \forall f',\ HasFDerivWithinAt\ f\ f'\ s\ x$$$

Lean4

/-- If `x` is not in the closure of `s`, then `f` has any derivative at `x` within `s`,
as this statement is empty. -/
theorem of_notMem_closure (h : x ∉ closure s) : HasFDerivWithinAt f f' s x :=
  .of_not_accPt (h ·.clusterPt.mem_closure)

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