α : Type u
β : Type v
ι : Type ?u.31786
π : ι → Type ?u.31791
inst✝ : TopologicalSpace α
s t u v : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : Set.Nonempty (s ∩ u)
h : closure u ∩ s ⊆ u
A : s ⊆ u ∪ closure uᶜ
⊢ Disjoint u (closure uᶜ)
α : Type u
β : Type v
ι : Type ?u.31786
π : ι → Type ?u.31791
inst✝ : TopologicalSpace α
s t u v : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : Set.Nonempty (s ∩ u)
h : closure u ∩ s ⊆ u
A : s ⊆ u ∪ closure uᶜ
⊢ s ⊆ u
apply hs.subset_left_of_subset_union hu isClosed_closure.isOpen_compl _ A h'u
no goals
α : Type u
β : Type v
ι : Type ?u.31786
π : ι → Type ?u.31791
inst✝ : TopologicalSpace α
s t u v : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : Set.Nonempty (s ∩ u)
h : closure u ∩ s ⊆ u
A : s ⊆ u ∪ closure uᶜ
⊢ Disjoint u (closure uᶜ)
exact disjoint_compl_right.mono_right (compl_subset_compl.2 subset_closure)
α : Type u
β : Type v
ι : Type ?u.31786
π : ι → Type ?u.31791
inst✝ : TopologicalSpace α
s t u v : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : Set.Nonempty (s ∩ u)
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
⊢ x ∈ u ∪ closure uᶜ
α : Type u
β : Type v
ι : Type ?u.31786
π : ι → Type ?u.31791
inst✝ : TopologicalSpace α
s t u v : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : Set.Nonempty (s ∩ u)
h : closure u ∩ s ⊆ u
⊢ s ⊆ u ∪ closure uᶜ
intro x hx
case pos
α : Type u
β : Type v
ι : Type ?u.31786
π : ι → Type ?u.31791
inst✝ : TopologicalSpace α
s t u v : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : Set.Nonempty (s ∩ u)
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∈ u
⊢ x ∈ u ∪ closure uᶜ

case neg
α : Type u
β : Type v
ι : Type ?u.31786
π : ι → Type ?u.31791
inst✝ : TopologicalSpace α
s t u v : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : Set.Nonempty (s ∩ u)
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : ¬x ∈ u
⊢ x ∈ u ∪ closure uᶜ
α : Type u
β : Type v
ι : Type ?u.31786
π : ι → Type ?u.31791
inst✝ : TopologicalSpace α
s t u v : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : Set.Nonempty (s ∩ u)
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
⊢ x ∈ u ∪ closure uᶜ
by_cases xu : x ∈ u
no goals
case pos
α : Type u
β : Type v
ι : Type ?u.31786
π : ι → Type ?u.31791
inst✝ : TopologicalSpace α
s t u v : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : Set.Nonempty (s ∩ u)
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∈ u
⊢ x ∈ u ∪ closure uᶜ
exact Or.inl xu
case neg.h
α : Type u
β : Type v
ι : Type ?u.31786
π : ι → Type ?u.31791
inst✝ : TopologicalSpace α
s t u v : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : Set.Nonempty (s ∩ u)
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : ¬x ∈ u
⊢ x ∈ closure uᶜ
case neg
α : Type u
β : Type v
ι : Type ?u.31786
π : ι → Type ?u.31791
inst✝ : TopologicalSpace α
s t u v : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : Set.Nonempty (s ∩ u)
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : ¬x ∈ u
⊢ x ∈ u ∪ closure uᶜ
right
case neg.h
α : Type u
β : Type v
ι : Type ?u.31786
π : ι → Type ?u.31791
inst✝ : TopologicalSpace α
s t u v : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : Set.Nonempty (s ∩ u)
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : ¬x ∈ u
h'x : x ∈ closure u
⊢ False
case neg.h
α : Type u
β : Type v
ι : Type ?u.31786
π : ι → Type ?u.31791
inst✝ : TopologicalSpace α
s t u v : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : Set.Nonempty (s ∩ u)
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : ¬x ∈ u
⊢ x ∈ closure uᶜ
intro h'x
no goals
case neg.h
α : Type u
β : Type v
ι : Type ?u.31786
π : ι → Type ?u.31791
inst✝ : TopologicalSpace α
s t u v : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : Set.Nonempty (s ∩ u)
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : ¬x ∈ u
h'x : x ∈ closure u
⊢ False
exact xu (h (mem_inter h'x hx))