isPreconnected_iUnion — Mathlib

English

If ⋂ i s_i is nonempty and each s_i is preconnected, then ⋃ i s_i is preconnected.

Русский

Если ⋂_i s_i непусто и каждый s_i предсоединён, то ⋃_i s_i предсоединено.

LaTeX

$$$$ \\left(\\bigcap_i s_i\\right) \\neq \\emptyset \\rightarrow (\\forall i, \\operatorname{IsPreconnected}(s_i)) \\rightarrow \\operatorname{IsPreconnected}\\left(\\bigcup_i s_i\\right). $$$$

Lean4

theorem isPreconnected_iUnion {ι : Sort*} {s : ι → Set α} (h₁ : (⋂ i, s i).Nonempty) (h₂ : ∀ i, IsPreconnected (s i)) :
    IsPreconnected (⋃ i, s i) :=
  Exists.elim h₁ fun f hf => isPreconnected_sUnion f _ hf (forall_mem_range.2 h₂)

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