iUnion_of_isOpen — Mathlib

English

If all sets s_i are open and f is differentiable on each s_i, then f is differentiable on the union.

Русский

Если все множества s_i открыты и функция дифференцируема на каждом s_i, то она дифференцируема на объединении.

LaTeX

$$DifferentiableOn 𝕜 f (⋃ i, s i) ↔ ∀ i, DifferentiableOn 𝕜 f (s i)$$

Lean4

/-- If a function is differentiable on open sets `s i`, it is differentiable on their union. -/
theorem iUnion_of_isOpen {ι : Type*} {s : ι → Set E} (hf : ∀ i : ι, DifferentiableOn 𝕜 f (s i))
    (hs : ∀ i, IsOpen (s i)) : DifferentiableOn 𝕜 f (⋃ i, s i) :=
  by
  rintro x ⟨si, ⟨i, rfl⟩, hxsi⟩
  exact (hf i).differentiableAt ((hs i).mem_nhds hxsi) |>.differentiableWithinAt

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