Theorem: IsPreconnected.iUnion_of_pairwise_exists_isPreconnected (Ray/Misc/Topology.lean)

State before:
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
s : ι → Set X
hsc : ∀ (i : ι), IsPreconnected (s i)
h :
  Pairwise fun i j =>
    (s i).Nonempty → (s j).Nonempty → ∃ u ⊆ ⋃ i, s i, (s i ∩ u).Nonempty ∧ (u ∩ s j).Nonempty ∧ IsPreconnected u
⊢ IsPreconnected (⋃ i, s i)
Tactic:
apply IsPreconnected.sUnion_of_pairwise_exists_isPreconnected (forall_mem_range.2 hsc)
State after:
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
s : ι → Set X
hsc : ∀ (i : ι), IsPreconnected (s i)
h :
  Pairwise fun i j =>
    (s i).Nonempty → (s j).Nonempty → ∃ u ⊆ ⋃ i, s i, (s i ∩ u).Nonempty ∧ (u ∩ s j).Nonempty ∧ IsPreconnected u
⊢ (range fun i => s i).Pairwise fun s_1 t =>
    s_1.Nonempty →
      t.Nonempty → ∃ u ⊆ (range fun i => s i).sUnion, (s_1 ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u

State before:
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
s : ι → Set X
hsc : ∀ (i : ι), IsPreconnected (s i)
h :
  Pairwise fun i j =>
    (s i).Nonempty → (s j).Nonempty → ∃ u ⊆ ⋃ i, s i, (s i ∩ u).Nonempty ∧ (u ∩ s j).Nonempty ∧ IsPreconnected u
⊢ (range fun i => s i).Pairwise fun s_1 t =>
    s_1.Nonempty →
      t.Nonempty → ∃ u ⊆ (range fun i => s i).sUnion, (s_1 ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
Tactic:
rintro _ ⟨i, rfl⟩ _ ⟨j, rfl⟩ hij
State after:
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
s : ι → Set X
hsc : ∀ (i : ι), IsPreconnected (s i)
h :
  Pairwise fun i j =>
    (s i).Nonempty → (s j).Nonempty → ∃ u ⊆ ⋃ i, s i, (s i ∩ u).Nonempty ∧ (u ∩ s j).Nonempty ∧ IsPreconnected u
i j : ι
hij : (fun i => s i) i ≠ (fun i => s i) j
⊢ ((fun i => s i) i).Nonempty →
    ((fun i => s i) j).Nonempty →
      ∃ u ⊆ (range fun i => s i).sUnion,
        ((fun i => s i) i ∩ u).Nonempty ∧ (u ∩ (fun i => s i) j).Nonempty ∧ IsPreconnected u

State before:
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
s : ι → Set X
hsc : ∀ (i : ι), IsPreconnected (s i)
h :
  Pairwise fun i j =>
    (s i).Nonempty → (s j).Nonempty → ∃ u ⊆ ⋃ i, s i, (s i ∩ u).Nonempty ∧ (u ∩ s j).Nonempty ∧ IsPreconnected u
i j : ι
hij : (fun i => s i) i ≠ (fun i => s i) j
⊢ ((fun i => s i) i).Nonempty →
    ((fun i => s i) j).Nonempty →
      ∃ u ⊆ (range fun i => s i).sUnion,
        ((fun i => s i) i ∩ u).Nonempty ∧ (u ∩ (fun i => s i) j).Nonempty ∧ IsPreconnected u
Tactic:
exact h (ne_of_apply_ne s hij)
State after:
no goals