α : Type u
β : Type v
ι✝ : Type ?u.8089
π : ι✝ → Type ?u.8094
inst✝ : TopologicalSpace α
s✝ t u v : Set α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsPreconnected (s i)
K : ∀ (i j : ι), ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j)) i j
⊢ IsPreconnected (⋃ (x : ι) (_ : x ∈ univ), s x)
α : Type u
β : Type v
ι✝ : Type ?u.8089
π : ι✝ → Type ?u.8094
inst✝ : TopologicalSpace α
s✝ t u v : Set α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsPreconnected (s i)
K : ∀ (i j : ι), ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j)) i j
⊢ IsPreconnected (⋃ (n : ι), s n)
rw [← biUnion_univ]
no goals
α : Type u
β : Type v
ι✝ : Type ?u.8089
π : ι✝ → Type ?u.8094
inst✝ : TopologicalSpace α
s✝ t u v : Set α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsPreconnected (s i)
K : ∀ (i j : ι), ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j)) i j
⊢ IsPreconnected (⋃ (x : ι) (_ : x ∈ univ), s x)
exact IsPreconnected.biUnion_of_reflTransGen (fun i _ => H i) fun i _ j _ => by
  simpa [mem_univ] using K i j
no goals
α : Type u
β : Type v
ι✝ : Type ?u.8089
π : ι✝ → Type ?u.8094
inst✝ : TopologicalSpace α
s✝ t u v : Set α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsPreconnected (s i)
K : ∀ (i j : ι), ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j)) i j
i : ι
x✝¹ : i ∈ univ
j : ι
x✝ : j ∈ univ
⊢ ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ univ) i j
simpa [mem_univ] using K i j