le_nhdsAdjoint_iff — Mathlib

English

A topology t is below nhdsAdjoint a f iff nhds a ≤ pure a ⊔ f and ∀ b ≠ a, IsOpen[t] { b }.

Русский

Топология t меньше nhdsAdjoint a f тогда и только тогда, когда nhds a ≤ pure a ⊔ f и ∀ b ≠ a, IsOpen[t] { b }.

LaTeX

$$theorem le_nhdsAdjoint_iff {α : Type*} (a : α) (f : Filter α) (t : TopologicalSpace α) : t ≤ nhdsAdjoint a f ↔ @nhds α t a ≤ pure a ⊔ f ∧ ∀ b ≠ a, IsOpen[t] { b }$$

Lean4

theorem le_nhdsAdjoint_iff {α : Type*} (a : α) (f : Filter α) (t : TopologicalSpace α) :
    t ≤ nhdsAdjoint a f ↔ @nhds α t a ≤ pure a ⊔ f ∧ ∀ b ≠ a, IsOpen[t] { b } := by
  simp only [le_nhdsAdjoint_iff', @isOpen_singleton_iff_nhds_eq_pure α t]

Похожие утверждения