α : Type u
β : Type v
ι : Type ?u.28526
π : ι → Type ?u.28531
inst✝ : TopologicalSpace α
s t u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
⊢ s ⊆ u ∨ s ⊆ v
α : Type u
β : Type v
ι : Type ?u.28526
π : ι → Type ?u.28531
inst✝ : TopologicalSpace α
s t u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : IsPreconnected s
⊢ s ⊆ u ∨ s ⊆ v
specialize hs u v hu hv hsuv
case inl
α : Type u
β : Type v
ι : Type ?u.28526
π : ι → Type ?u.28531
inst✝ : TopologicalSpace α
s t u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
hsu : s ∩ u = ∅
⊢ s ⊆ u ∨ s ⊆ v

case inr
α : Type u
β : Type v
ι : Type ?u.28526
π : ι → Type ?u.28531
inst✝ : TopologicalSpace α
s t u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
hsu : Set.Nonempty (s ∩ u)
⊢ s ⊆ u ∨ s ⊆ v
α : Type u
β : Type v
ι : Type ?u.28526
π : ι → Type ?u.28531
inst✝ : TopologicalSpace α
s t u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
⊢ s ⊆ u ∨ s ⊆ v
obtain hsu | hsu := (s ∩ u).eq_empty_or_nonempty
no goals
case inl
α : Type u
β : Type v
ι : Type ?u.28526
π : ι → Type ?u.28531
inst✝ : TopologicalSpace α
s t u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
hsu : s ∩ u = ∅
⊢ s ⊆ u ∨ s ⊆ v
exact Or.inr ((Set.disjoint_iff_inter_eq_empty.2 hsu).subset_right_of_subset_union hsuv)
case inr
α : Type u
β : Type v
ι : Type ?u.28526
π : ι → Type ?u.28531
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 : ¬Set.Nonempty (s ∩ (u ∩ v)) → ¬Set.Nonempty (s ∩ v)
⊢ s ⊆ u ∨ s ⊆ v
case inr
α : Type u
β : Type v
ι : Type ?u.28526
π : ι → Type ?u.28531
inst✝ : TopologicalSpace α
s t u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
hsu : Set.Nonempty (s ∩ u)
⊢ s ⊆ u ∨ s ⊆ v
replace hs := mt (hs hsu)
case inr
α : Type u
β : Type v
ι : Type ?u.28526
π : ι → Type ?u.28531
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 : Disjoint s ∅ → Disjoint s v
⊢ s ⊆ u ∨ s ⊆ v
case inr
α : Type u
β : Type v
ι : Type ?u.28526
π : ι → Type ?u.28531
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 : ¬Set.Nonempty (s ∩ (u ∩ v)) → ¬Set.Nonempty (s ∩ v)
⊢ s ⊆ u ∨ s ⊆ v
simp_rw [Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty,
  disjoint_iff_inter_eq_empty.1 huv] at hs
no goals
case inr
α : Type u
β : Type v
ι : Type ?u.28526
π : ι → Type ?u.28531
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 : Disjoint s ∅ → Disjoint s v
⊢ s ⊆ u ∨ s ⊆ v
exact Or.inl ((hs s.disjoint_empty).subset_left_of_subset_union hsuv)