case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.4785
π : ι → Type ?u.4790
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ : Set α
S : Set (Set α)
K : DirectedOn (fun x x_1 => x ⊆ x_1) S
H : ∀ (s : Set α), s ∈ S → IsPreconnected s
u v : Set α
hu : IsOpen u
hv : IsOpen v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
⊢ Set.Nonempty (⋃₀ S ∩ (u ∩ v))
α : Type u
β : Type v
ι : Type ?u.4785
π : ι → Type ?u.4790
inst✝ : TopologicalSpace α
s t u v : Set α
S : Set (Set α)
K : DirectedOn (fun x x_1 => x ⊆ x_1) S
H : ∀ (s : Set α), s ∈ S → IsPreconnected s
⊢ IsPreconnected (⋃₀ S)
rintro u v hu hv Huv ⟨a, ⟨s, hsS, has⟩, hau⟩ ⟨b, ⟨t, htS, hbt⟩, hbv⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.4785
π : ι → Type ?u.4790
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ : Set α
S : Set (Set α)
K : DirectedOn (fun x x_1 => x ⊆ x_1) S
H : ∀ (s : Set α), s ∈ S → IsPreconnected s
u v : Set α
hu : IsOpen u
hv : IsOpen v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
r : Set α
hrS : r ∈ S
hsr : s ⊆ r
htr : t ⊆ r
⊢ Set.Nonempty (⋃₀ S ∩ (u ∩ v))
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.4785
π : ι → Type ?u.4790
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ : Set α
S : Set (Set α)
K : DirectedOn (fun x x_1 => x ⊆ x_1) S
H : ∀ (s : Set α), s ∈ S → IsPreconnected s
u v : Set α
hu : IsOpen u
hv : IsOpen v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
⊢ Set.Nonempty (⋃₀ S ∩ (u ∩ v))
obtain ⟨r, hrS, hsr, htr⟩ : ∃ r ∈ S, s ⊆ r ∧ t ⊆ r := K s hsS t htS
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.4785
π : ι → Type ?u.4790
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ : Set α
S : Set (Set α)
K : DirectedOn (fun x x_1 => x ⊆ x_1) S
H : ∀ (s : Set α), s ∈ S → IsPreconnected s
u v : Set α
hu : IsOpen u
hv : IsOpen v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
r : Set α
hrS : r ∈ S
hsr : s ⊆ r
htr : t ⊆ r
Hnuv : Set.Nonempty (r ∩ (u ∩ v))
⊢ Set.Nonempty (⋃₀ S ∩ (u ∩ v))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.4785
π : ι → Type ?u.4790
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ : Set α
S : Set (Set α)
K : DirectedOn (fun x x_1 => x ⊆ x_1) S
H : ∀ (s : Set α), s ∈ S → IsPreconnected s
u v : Set α
hu : IsOpen u
hv : IsOpen v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
r : Set α
hrS : r ∈ S
hsr : s ⊆ r
htr : t ⊆ r
⊢ Set.Nonempty (⋃₀ S ∩ (u ∩ v))
have Hnuv : (r ∩ (u ∩ v)).Nonempty :=
  H _ hrS u v hu hv ((subset_sUnion_of_mem hrS).trans Huv) ⟨a, hsr has, hau⟩ ⟨b, htr hbt, hbv⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.4785
π : ι → Type ?u.4790
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ : Set α
S : Set (Set α)
K : DirectedOn (fun x x_1 => x ⊆ x_1) S
H : ∀ (s : Set α), s ∈ S → IsPreconnected s
u v : Set α
hu : IsOpen u
hv : IsOpen v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
r : Set α
hrS : r ∈ S
hsr : s ⊆ r
htr : t ⊆ r
Hnuv : Set.Nonempty (r ∩ (u ∩ v))
Kruv : r ∩ (u ∩ v) ⊆ ⋃₀ S ∩ (u ∩ v)
⊢ Set.Nonempty (⋃₀ S ∩ (u ∩ v))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.4785
π : ι → Type ?u.4790
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ : Set α
S : Set (Set α)
K : DirectedOn (fun x x_1 => x ⊆ x_1) S
H : ∀ (s : Set α), s ∈ S → IsPreconnected s
u v : Set α
hu : IsOpen u
hv : IsOpen v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
r : Set α
hrS : r ∈ S
hsr : s ⊆ r
htr : t ⊆ r
Hnuv : Set.Nonempty (r ∩ (u ∩ v))
⊢ Set.Nonempty (⋃₀ S ∩ (u ∩ v))
have Kruv : r ∩ (u ∩ v) ⊆ ⋃₀ S ∩ (u ∩ v) := inter_subset_inter_left _ (subset_sUnion_of_mem hrS)
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.4785
π : ι → Type ?u.4790
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ : Set α
S : Set (Set α)
K : DirectedOn (fun x x_1 => x ⊆ x_1) S
H : ∀ (s : Set α), s ∈ S → IsPreconnected s
u v : Set α
hu : IsOpen u
hv : IsOpen v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
r : Set α
hrS : r ∈ S
hsr : s ⊆ r
htr : t ⊆ r
Hnuv : Set.Nonempty (r ∩ (u ∩ v))
Kruv : r ∩ (u ∩ v) ⊆ ⋃₀ S ∩ (u ∩ v)
⊢ Set.Nonempty (⋃₀ S ∩ (u ∩ v))
exact Hnuv.mono Kruv