iteratedDerivWithin_of_isOpen_eq_iterate

English

For open s, iteratedDerivWithin n f s equals the n-th iterate of deriv: iteratedDerivWithin n f s = deriv^[n] f on s.

Русский

Пусть s открыто. Тогда iteratedDerivWithin n f s = deriv^[n] f на s.

LaTeX

$$$\\IsOpen s \\Rightarrow EqOn (iteratedDerivWithin n f s) (Nat.iterate deriv n f) s$$$

Lean4

theorem iteratedDerivWithin_of_isOpen_eq_iterate (hs : IsOpen s) : EqOn (iteratedDerivWithin n f s) (deriv^[n] f) s :=
  by
  apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen hs)
  rw [iteratedDeriv_eq_iterate]
  exact Set.eqOn_refl _ _

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