differentiableOn_iUnion_iff_of_isOpen

English

Equivalence between differentiability on an iUnion and differentiability on each component under openness.

Русский

Эквивалентность между дифференцируемостью на iUnion и дифференцируемостью на каждом компоненте при условии открытости.

LaTeX

$$DifferentiableOn 𝕜 f (Set.iUnion fun i => s i) ↔ ∀ i, DifferentiableOn 𝕜 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 differentiableOn_iUnion_iff_of_isOpen {ι : Type*} {s : ι → Set E} (hs : ∀ i, IsOpen (s i)) :
    DifferentiableOn 𝕜 f (⋃ i, s i) ↔ ∀ i : ι, DifferentiableOn 𝕜 f (s i) :=
  ⟨fun h i ↦ h.mono <| subset_iUnion_of_subset i fun _ a ↦ a, fun h ↦ DifferentiableOn.iUnion_of_isOpen h hs⟩

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