English
A set s is connected iff for every finite family of open sets covering s such that pairwise intersections inside s are empty, there exists a member u of the family containing s.
Русский
Множество s связано тогда и только тогда, когда для каждого конечного семейства открытых множеств, покрывающего s и внутри которых попарно пустые пересечения, существует элемент u, содержащий s.
LaTeX
$$$IsConnected\; s \iff \forall U \text{ finite}, \big( \forall u\in U, IsOpen u \big) \to (s \subseteq \bigcup U) \to \exists u\in U, s \subseteq u$$$
Lean4
/-- A set `s` is connected if and only if
for every cover by a finite collection of open sets that are pairwise disjoint on `s`,
it is contained in one of the members of the collection. -/
theorem isConnected_iff_sUnion_disjoint_open {s : Set α} :
IsConnected s ↔
∀ U : Finset (Set α),
(∀ u v : Set α, u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
(∀ u ∈ U, IsOpen u) → (s ⊆ ⋃₀ ↑U) → ∃ u ∈ U, s ⊆ u :=
by
rw [IsConnected, isPreconnected_iff_subset_of_disjoint]
classical
refine ⟨fun ⟨hne, h⟩ U hU hUo hsU => ?_, fun h => ⟨?_, fun u v hu hv hs hsuv => ?_⟩⟩
·
induction U using Finset.induction_on with
| empty => exact absurd (by simpa using hsU) hne.not_subset_empty
| insert u U uU
IH =>
simp only [← forall_cond_comm, Finset.forall_mem_insert, Finset.exists_mem_insert, Finset.coe_insert,
sUnion_insert, implies_true, true_and] at *
refine (h _ hUo.1 (⋃₀ ↑U) (isOpen_sUnion hUo.2) hsU ?_).imp_right ?_
· refine subset_empty_iff.1 fun x ⟨hxs, hxu, v, hvU, hxv⟩ => ?_
exact ne_of_mem_of_not_mem hvU uU (hU.1 v hvU ⟨x, hxs, hxu, hxv⟩).symm
· exact IH (fun u hu => (hU.2 u hu).2) hUo.2
· simpa [subset_empty_iff, nonempty_iff_ne_empty] using h ∅
· rw [← not_nonempty_iff_eq_empty] at hsuv
have := hsuv; rw [inter_comm u] at this
simpa [*, or_imp, forall_and] using h { u, v }
