English
A topological order relation t ≤ nhdsAdjoint a f is equivalent to nhds a ≤ pure a ⊔ f and ∀ b ≠ a, nhds b = pure b.
Русский
Порядковое неравенство t ≤ nhdsAdjoint(a,f) эквивалентно nhds a ≤ pure a ⊔ f и ∀ b ≠ a, nhds b = pure b.
LaTeX
$$theorem le_nhdsAdjoint_iff' {a : α} {f : Filter α} {t : TopologicalSpace α} : t ≤ nhdsAdjoint a f ↔ @nhds α t a ≤ pure a ⊔ f ∧ ∀ b ≠ a, @nhds α t b = pure b$$
Lean4
theorem le_nhdsAdjoint_iff' {a : α} {f : Filter α} {t : TopologicalSpace α} :
t ≤ nhdsAdjoint a f ↔ @nhds α t a ≤ pure a ⊔ f ∧ ∀ b ≠ a, @nhds α t b = pure b := by
classical simp_rw [le_iff_nhds, nhds_nhdsAdjoint, forall_update_iff, (pure_le_nhds _).ge_iff_eq']
