of_finite — Mathlib

English

If s is a finite set, then HasFDerivWithinAt f f' s x holds, for any f, f', x.

Русский

Если s конечное множество, то HasFDerivWithinAt f f' s x выполняется для любых f, f', x.

LaTeX

$$$$s\\text{ finite } \\Rightarrow \\text{HasFDerivWithinAt } f\\,f'\\,s\\,x.$$$$

Lean4

theorem of_finite (h : s.Finite) : HasFDerivWithinAt f f' s x := by
  induction s, h using Set.Finite.induction_on with
  | empty => exact .empty
  | insert _ _ ih => exact ih.insert'

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