α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 b = pure b
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
⊢ 𝓝 b = pure b
letI := nhdsAdjoint a f
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 b ≤ pure b

case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
⊢ pure b ≤ 𝓝 b
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 b = pure b
apply le_antisymm
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
hU : U ∈ pure b
⊢ U ∈ 𝓝 b
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 b ≤ pure b
intro U hU
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
hU : U ∈ pure b
⊢ ∃ t, t ⊆ U ∧ IsOpen t ∧ b ∈ t
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
hU : U ∈ pure b
⊢ U ∈ 𝓝 b
rw [mem_nhds_iff]
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
hU : U ∈ pure b
⊢ {b} ⊆ U ∧ IsOpen {b} ∧ b ∈ {b}
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
hU : U ∈ pure b
⊢ ∃ t, t ⊆ U ∧ IsOpen t ∧ b ∈ t
use {b}
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
hU : U ∈ pure b
⊢ b ∈ U ∧ IsOpen {b}
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
hU : U ∈ pure b
⊢ {b} ⊆ U ∧ IsOpen {b} ∧ b ∈ {b}
simp only [and_true_iff, singleton_subset_iff, mem_singleton]
no goals
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
U : Set α
hU : U ∈ pure b
⊢ b ∈ U ∧ IsOpen {b}
refine' ⟨hU, fun ha => (h.symm ha).elim⟩
no goals
case a
α✝ : Type u
β : Type v
α : Type u_1
a : α
f : Filter α
b : α
h : b ≠ a
this : TopologicalSpace α := nhdsAdjoint a f
⊢ pure b ≤ 𝓝 b
exact @pure_le_nhds α (nhdsAdjoint a f) b