α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
⊢ IsPreconnected (⋃ (n : ι) (_ : n ∈ t), s n)
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
⊢ IsPreconnected (⋃ (n : ι) (_ : n ∈ t), s n)
let R := fun i j : ι => (s i ∩ s j).Nonempty ∧ i ∈ t
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
P :
  ∀ (i : ι),
    i ∈ t →
      ∀ (j : ι), j ∈ t → ReflTransGen R i j → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
⊢ IsPreconnected (⋃ (n : ι) (_ : n ∈ t), s n)
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
⊢ IsPreconnected (⋃ (n : ι) (_ : n ∈ t), s n)
have P : ∀ i, i ∈ t → ∀ j, j ∈ t → ReflTransGen R i j →
    ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j) := fun i hi j hj h => by
  induction h
  case refl =>
    refine ⟨{i}, singleton_subset_iff.mpr hi, mem_singleton i, mem_singleton i, ?_⟩
    rw [biUnion_singleton]
    exact H i hi
  case tail j k _ hjk ih =>
    obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2
    refine ⟨insert k p, insert_subset.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip, mem_insert k p, ?_⟩
    rw [biUnion_insert]
    refine (H k hj).union' (hjk.1.mono ?_) hp
    rw [inter_comm]
    exact inter_subset_inter_right _ (subset_biUnion_of_mem hjp)
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
P :
  ∀ (i : ι),
    i ∈ t →
      ∀ (j : ι), j ∈ t → ReflTransGen R i j → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
⊢ ∀ (x : α),
    (x ∈ ⋃ (n : ι) (_ : n ∈ t), s n) →
      ∀ (y : α),
        (y ∈ ⋃ (n : ι) (_ : n ∈ t), s n) →
          ∃ t_1, (t_1 ⊆ ⋃ (n : ι) (_ : n ∈ t), s n) ∧ x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
P :
  ∀ (i : ι),
    i ∈ t →
      ∀ (j : ι), j ∈ t → ReflTransGen R i j → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
⊢ IsPreconnected (⋃ (n : ι) (_ : n ∈ t), s n)
refine' isPreconnected_of_forall_pair _
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
P :
  ∀ (i : ι),
    i ∈ t →
      ∀ (j : ι), j ∈ t → ReflTransGen R i j → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
x : α
hx : x ∈ ⋃ (n : ι) (_ : n ∈ t), s n
y : α
hy : y ∈ ⋃ (n : ι) (_ : n ∈ t), s n
⊢ ∃ t_1, (t_1 ⊆ ⋃ (n : ι) (_ : n ∈ t), s n) ∧ x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
P :
  ∀ (i : ι),
    i ∈ t →
      ∀ (j : ι), j ∈ t → ReflTransGen R i j → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
⊢ ∀ (x : α),
    (x ∈ ⋃ (n : ι) (_ : n ∈ t), s n) →
      ∀ (y : α),
        (y ∈ ⋃ (n : ι) (_ : n ∈ t), s n) →
          ∃ t_1, (t_1 ⊆ ⋃ (n : ι) (_ : n ∈ t), s n) ∧ x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
intro x hx y hy
case intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
P :
  ∀ (i : ι),
    i ∈ t →
      ∀ (j : ι), j ∈ t → ReflTransGen R i j → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
x : α
hx : x ∈ ⋃ (n : ι) (_ : n ∈ t), s n
y : α
hy : y ∈ ⋃ (n : ι) (_ : n ∈ t), s n
i : ι
hi : i ∈ t
hxi : x ∈ s i
⊢ ∃ t_1, (t_1 ⊆ ⋃ (n : ι) (_ : n ∈ t), s n) ∧ x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
P :
  ∀ (i : ι),
    i ∈ t →
      ∀ (j : ι), j ∈ t → ReflTransGen R i j → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
x : α
hx : x ∈ ⋃ (n : ι) (_ : n ∈ t), s n
y : α
hy : y ∈ ⋃ (n : ι) (_ : n ∈ t), s n
⊢ ∃ t_1, (t_1 ⊆ ⋃ (n : ι) (_ : n ∈ t), s n) ∧ x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
obtain ⟨i : ι, hi : i ∈ t, hxi : x ∈ s i⟩ := mem_iUnion₂.1 hx
case intro.intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
P :
  ∀ (i : ι),
    i ∈ t →
      ∀ (j : ι), j ∈ t → ReflTransGen R i j → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
x : α
hx : x ∈ ⋃ (n : ι) (_ : n ∈ t), s n
y : α
hy : y ∈ ⋃ (n : ι) (_ : n ∈ t), s n
i : ι
hi : i ∈ t
hxi : x ∈ s i
j : ι
hj : j ∈ t
hyj : y ∈ s j
⊢ ∃ t_1, (t_1 ⊆ ⋃ (n : ι) (_ : n ∈ t), s n) ∧ x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
case intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
P :
  ∀ (i : ι),
    i ∈ t →
      ∀ (j : ι), j ∈ t → ReflTransGen R i j → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
x : α
hx : x ∈ ⋃ (n : ι) (_ : n ∈ t), s n
y : α
hy : y ∈ ⋃ (n : ι) (_ : n ∈ t), s n
i : ι
hi : i ∈ t
hxi : x ∈ s i
⊢ ∃ t_1, (t_1 ⊆ ⋃ (n : ι) (_ : n ∈ t), s n) ∧ x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
obtain ⟨j : ι, hj : j ∈ t, hyj : y ∈ s j⟩ := mem_iUnion₂.1 hy
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
P :
  ∀ (i : ι),
    i ∈ t →
      ∀ (j : ι), j ∈ t → ReflTransGen R i j → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
x : α
hx : x ∈ ⋃ (n : ι) (_ : n ∈ t), s n
y : α
hy : y ∈ ⋃ (n : ι) (_ : n ∈ t), s n
i : ι
hi : i ∈ t
hxi : x ∈ s i
j : ι
hj : j ∈ t
hyj : y ∈ s j
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
⊢ ∃ t_1, (t_1 ⊆ ⋃ (n : ι) (_ : n ∈ t), s n) ∧ x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
case intro.intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
P :
  ∀ (i : ι),
    i ∈ t →
      ∀ (j : ι), j ∈ t → ReflTransGen R i j → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
x : α
hx : x ∈ ⋃ (n : ι) (_ : n ∈ t), s n
y : α
hy : y ∈ ⋃ (n : ι) (_ : n ∈ t), s n
i : ι
hi : i ∈ t
hxi : x ∈ s i
j : ι
hj : j ∈ t
hyj : y ∈ s j
⊢ ∃ t_1, (t_1 ⊆ ⋃ (n : ι) (_ : n ∈ t), s n) ∧ x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
obtain ⟨p, hpt, hip, hjp, hp⟩ := P i hi j hj (K i hi j hj)
no goals
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
P :
  ∀ (i : ι),
    i ∈ t →
      ∀ (j : ι), j ∈ t → ReflTransGen R i j → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
x : α
hx : x ∈ ⋃ (n : ι) (_ : n ∈ t), s n
y : α
hy : y ∈ ⋃ (n : ι) (_ : n ∈ t), s n
i : ι
hi : i ∈ t
hxi : x ∈ s i
j : ι
hj : j ∈ t
hyj : y ∈ s j
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
⊢ ∃ t_1, (t_1 ⊆ ⋃ (n : ι) (_ : n ∈ t), s n) ∧ x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
exact ⟨⋃ j ∈ p, s j, biUnion_subset_biUnion_left hpt, mem_biUnion hip hxi,
  mem_biUnion hjp hyj, hp⟩
case refl
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ ∃ p, p ⊆ t ∧ i ∈ p ∧ i ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)

case tail
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j b✝ c✝ : ι
a✝¹ : ReflTransGen R i b✝
a✝ : R b✝ c✝
a_ih✝ : b✝ ∈ t → ∃ p, p ⊆ t ∧ i ∈ p ∧ b✝ ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
hj : c✝ ∈ t
⊢ ∃ p, p ⊆ t ∧ i ∈ p ∧ c✝ ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : j ∈ t
h : ReflTransGen R i j
⊢ ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
induction h
case tail
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j b✝ c✝ : ι
a✝¹ : ReflTransGen R i b✝
a✝ : R b✝ c✝
a_ih✝ : b✝ ∈ t → ∃ p, p ⊆ t ∧ i ∈ p ∧ b✝ ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
hj : c✝ ∈ t
⊢ ∃ p, p ⊆ t ∧ i ∈ p ∧ c✝ ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
case refl
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ ∃ p, p ⊆ t ∧ i ∈ p ∧ i ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)

case tail
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j b✝ c✝ : ι
a✝¹ : ReflTransGen R i b✝
a✝ : R b✝ c✝
a_ih✝ : b✝ ∈ t → ∃ p, p ⊆ t ∧ i ∈ p ∧ b✝ ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
hj : c✝ ∈ t
⊢ ∃ p, p ⊆ t ∧ i ∈ p ∧ c✝ ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
case refl =>
  refine ⟨{i}, singleton_subset_iff.mpr hi, mem_singleton i, mem_singleton i, ?_⟩
  rw [biUnion_singleton]
  exact H i hi
no goals
case tail
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j b✝ c✝ : ι
a✝¹ : ReflTransGen R i b✝
a✝ : R b✝ c✝
a_ih✝ : b✝ ∈ t → ∃ p, p ⊆ t ∧ i ∈ p ∧ b✝ ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
hj : c✝ ∈ t
⊢ ∃ p, p ⊆ t ∧ i ∈ p ∧ c✝ ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
case tail j k _ hjk ih =>
  obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2
  refine ⟨insert k p, insert_subset.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip, mem_insert k p, ?_⟩
  rw [biUnion_insert]
  refine (H k hj).union' (hjk.1.mono ?_) hp
  rw [inter_comm]
  exact inter_subset_inter_right _ (subset_biUnion_of_mem hjp)
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ IsPreconnected (⋃ (j : ι) (_ : j ∈ {i}), s j)
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ ∃ p, p ⊆ t ∧ i ∈ p ∧ i ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
refine ⟨{i}, singleton_subset_iff.mpr hi, mem_singleton i, mem_singleton i, ?_⟩
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ IsPreconnected (s i)
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ IsPreconnected (⋃ (j : ι) (_ : j ∈ {i}), s j)
rw [biUnion_singleton]
no goals
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ IsPreconnected (s i)
exact H i hi
case intro.intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
⊢ ∃ p, p ⊆ t ∧ i ∈ p ∧ k ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
hj : k ∈ t
⊢ ∃ p, p ⊆ t ∧ i ∈ p ∧ k ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2
case intro.intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
⊢ IsPreconnected (⋃ (j : ι) (_ : j ∈ insert k p), s j)
case intro.intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
⊢ ∃ p, p ⊆ t ∧ i ∈ p ∧ k ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
refine ⟨insert k p, insert_subset.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip, mem_insert k p, ?_⟩
case intro.intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
⊢ IsPreconnected (s k ∪ ⋃ (x : ι) (_ : x ∈ p), s x)
case intro.intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
⊢ IsPreconnected (⋃ (j : ι) (_ : j ∈ insert k p), s j)
rw [biUnion_insert]
case intro.intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
⊢ s j ∩ s k ⊆ s k ∩ ⋃ (x : ι) (_ : x ∈ p), s x
case intro.intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
⊢ IsPreconnected (s k ∪ ⋃ (x : ι) (_ : x ∈ p), s x)
refine (H k hj).union' (hjk.1.mono ?_) hp
case intro.intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
⊢ s k ∩ s j ⊆ s k ∩ ⋃ (x : ι) (_ : x ∈ p), s x
case intro.intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
⊢ s j ∩ s k ⊆ s k ∩ ⋃ (x : ι) (_ : x ∈ p), s x
rw [inter_comm]
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.5558
π : ι✝ → Type ?u.5563
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
ι : Type u_1
t : Set ι
s : ι → Set α
H : ∀ (i : ι), i ∈ t → IsPreconnected (s i)
K : ∀ (i : ι), i ∈ t → ∀ (j : ι), j ∈ t → ReflTransGen (fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j => Set.Nonempty (s i ∩ s j) ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ (j : ι) (_ : j ∈ p), s j)
⊢ s k ∩ s j ⊆ s k ∩ ⋃ (x : ι) (_ : x ∈ p), s x
exact inter_subset_inter_right _ (subset_biUnion_of_mem hjp)