α : Type u
β : Type v
ι : Type ?u.29699
π : ι → Type ?u.29704
inst✝ : TopologicalSpace α
s t u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hs : IsPreconnected s
hsv : ¬Disjoint s v
⊢ False
α : Type u
β : Type v
ι : Type ?u.29699
π : ι → Type ?u.29704
inst✝ : TopologicalSpace α
s t u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hs : IsPreconnected s
⊢ Disjoint s v
by_contra hsv
α : Type u
β : Type v
ι : Type ?u.29699
π : ι → Type ?u.29704
inst✝ : TopologicalSpace α
s t u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hs : IsPreconnected s
hsv : Set.Nonempty (s ∩ v)
⊢ False
α : Type u
β : Type v
ι : Type ?u.29699
π : ι → Type ?u.29704
inst✝ : TopologicalSpace α
s t u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hs : IsPreconnected s
hsv : ¬Disjoint s v
⊢ False
rw [not_disjoint_iff_nonempty_inter] at hsv
case intro.intro
α : Type u
β : Type v
ι : Type ?u.29699
π : ι → Type ?u.29704
inst✝ : TopologicalSpace α
s t u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hs : IsPreconnected s
hsv : Set.Nonempty (s ∩ v)
x : α
left✝ : x ∈ s
hx : x ∈ u ∩ v
⊢ False
α : Type u
β : Type v
ι : Type ?u.29699
π : ι → Type ?u.29704
inst✝ : TopologicalSpace α
s t u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hs : IsPreconnected s
hsv : Set.Nonempty (s ∩ v)
⊢ False
obtain ⟨x, _, hx⟩ := hs u v hu hv hsuv hsu hsv
no goals
case intro.intro
α : Type u
β : Type v
ι : Type ?u.29699
π : ι → Type ?u.29704
inst✝ : TopologicalSpace α
s t u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : Set.Nonempty (s ∩ u)
hs : IsPreconnected s
hsv : Set.Nonempty (s ∩ v)
x : α
left✝ : x ∈ s
hx : x ∈ u ∩ v
⊢ False
exact Set.disjoint_iff.1 huv hx