continuousOn_iUnion_iff_of_isOpen

English

If every s_i is open, then continuity on the union is equivalent to continuity on each s_i.

Русский

Если все s_i открыты, то непрерывность на объединении эквивалентна непрерывности на каждом s_i.

LaTeX

$$$\\forall i,\\; \\text{IsOpen } s_i \\Rightarrow (\\text{ContinuousOn } f (\\bigcup_i s_i) \\iff \\forall i, \\text{ContinuousOn } f (s_i))$$$

Lean4

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

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