continuous_of_continuousOn_iUnion_of_isOpen

English

If a function is continuous on all members of an indexed family of open sets whose union is the whole space, then the function is continuous on the whole space.

Русский

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

LaTeX

$$$\\forall i,\\; \\text{ContinuousOn } f (s_i) \\land (\\bigcup_i s_i = \\mathrm{univ}) \\Rightarrow \\text{ContinuousOn } f (\\mathrm{univ})$$$

Lean4

theorem continuous_of_continuousOn_iUnion_of_isOpen {ι : Type*} {s : ι → Set α} (hf : ∀ i : ι, ContinuousOn f (s i))
    (hs : ∀ i, IsOpen (s i)) (hs' : ⋃ i, s i = univ) : Continuous f :=
  by
  rw [← continuousOn_univ, ← hs']
  exact ContinuousOn.iUnion_of_isOpen hf hs

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