Theorems · Theorem · general topology

TopologicalSpace.nhds_mkOfNhds_filterBasis

∀ {α : Type u} (B : α → FilterBasis α) (a : α),
  (∀ (x : α), ∀ n ∈ B x, x ∈ n) →
    (∀ (x : α), ∀ n ∈ B x, ∃ n₁ ∈ B x, ∀ x' ∈ n₁, ∃ n₂ ∈ B x', n₂ ⊆ n) → nhds a = (B a).filter

Defined in

Mathlib.Topology.Order

Cited by

0 results in Mathlib

Foundations

Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound