English
The iUnion of a chain of preconnected sets, indexed by a subset t of a linearly ordered archimedean type, is preconnected provided neighboring sets meet and t is order-connected.
Русский
Объединение iUnion цепочки предсоединяемых множеств, индексируемой подмножеством t линейно упорядоченного типа, предсоединено, если ближайшие множества встречаются и t упорядочно-связно.
LaTeX
$$$ht : OrdConnected\ t \rightarrow (\forall n \in t, IsPreconnected (s n)) \rightarrow (\forall n \in t, succ n \in t \rightarrow (s n \cap s (succ n)).Nonempty) \rightarrow IsPreconnected (\bigcup n \in t, s n)$$$
Lean4
/-- The iUnion of preconnected sets indexed by a subset of a type with an archimedean successor
(like `ℕ` or `ℤ`) such that any two neighboring sets meet is preconnected. -/
theorem biUnion_of_chain {s : β → Set α} {t : Set β} (ht : OrdConnected t) (H : ∀ n ∈ t, IsPreconnected (s n))
(K : ∀ n : β, n ∈ t → succ n ∈ t → (s n ∩ s (succ n)).Nonempty) : IsPreconnected (⋃ n ∈ t, s n) :=
by
have h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t := fun hi hj hk => ht.out hi hj (Ico_subset_Icc_self hk)
have h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t := fun hi hj hk =>
ht.out hi hj ⟨hk.1.trans <| le_succ _, succ_le_of_lt hk.2⟩
have h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty := fun hi hj hk =>
K _ (h1 hi hj hk) (h2 hi hj hk)
refine IsPreconnected.biUnion_of_reflTransGen H fun i hi j hj => ?_
exact
reflTransGen_of_succ _ (fun k hk => ⟨h3 hi hj hk, h1 hi hj hk⟩) fun k hk =>
⟨by rw [inter_comm]; exact h3 hj hi hk, h2 hj hi hk⟩
