Theorem: UniformSpace.nhds_inf_uniform_nhds_eq_bot (RMT4/uniform.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s : Set α
hf : 𝓝 a ⊓ 𝓟 s = ⊥
⊢ 𝓝 a ⊓ 𝓝ᵘ s = ⊥
Tactic:
rw [← uniform_nhds_set_singleton] at hf ⊢
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s : Set α
hf : 𝓝ᵘ {a} ⊓ 𝓟 s = ⊥
⊢ 𝓝ᵘ {a} ⊓ 𝓝ᵘ s = ⊥

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s : Set α
hf : 𝓝ᵘ {a} ⊓ 𝓟 s = ⊥
⊢ 𝓝ᵘ {a} ⊓ 𝓝ᵘ s = ⊥
Tactic:
exact uniform_nhds_inf_uniform_nhds_eq_bot hf
State after:
no goals