mdifferentiableOn_iUnion_iff_of_isOpen

English

If a family of sets s_i is open, then differentiability on the union equals differentiability on all pieces.

Русский

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

LaTeX

$$$$IsOpen(s_i) \\;\\text{for all } i \\Rightarrow (MDifferentiableOn I I' f (\\bigcup_i s_i) \\iff \\forall i, MDifferentiableOn I I' f (s_i))$$$$

Lean4

/-- A function is differentiable on a union of open sets `s i`
iff it is differentiable on each `s i`. -/
theorem mdifferentiableOn_iUnion_iff_of_isOpen {ι : Type*} {s : ι → Set M} (hs : ∀ i, IsOpen (s i)) :
    MDifferentiableOn I I' f (⋃ i, s i) ↔ ∀ i : ι, MDifferentiableOn I I' f (s i) :=
  ⟨fun h i ↦ h.mono <| subset_iUnion_of_subset i fun _ a ↦ a, fun h ↦ MDifferentiableOn.iUnion_of_isOpen h hs⟩

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