α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
x : α
inst✝ : NeBot (𝓝[{x}ᶜ] x)
y : α
⊢ y ∈ closure ({x}ᶜ)
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
x : α
inst✝ : NeBot (𝓝[{x}ᶜ] x)
⊢ Dense ({x}ᶜ)
intro y
case inl
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
y : α
inst✝ : NeBot (𝓝[{y}ᶜ] y)
⊢ y ∈ closure ({y}ᶜ)

case inr
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
x : α
inst✝ : NeBot (𝓝[{x}ᶜ] x)
y : α
hne : y ≠ x
⊢ y ∈ closure ({x}ᶜ)
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
x : α
inst✝ : NeBot (𝓝[{x}ᶜ] x)
y : α
⊢ y ∈ closure ({x}ᶜ)
rcases eq_or_ne y x with (rfl | hne)
no goals
case inl
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
y : α
inst✝ : NeBot (𝓝[{y}ᶜ] y)
⊢ y ∈ closure ({y}ᶜ)
rwa [mem_closure_iff_nhdsWithin_neBot]
no goals
case inr
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝¹ : TopologicalSpace α
x : α
inst✝ : NeBot (𝓝[{x}ᶜ] x)
y : α
hne : y ≠ x
⊢ y ∈ closure ({x}ᶜ)
exact subset_closure hne