Ctop.Realizer.mem_nhds

theorem Ctop.Realizer.mem_nhds : ∀ {α : Type u_1} [T : TopologicalSpace α] (F : Ctop.Realizer α) {s : Set α} {a : α}, s ∈ nhds a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s

This theorem states that for any type `α` with a given topological space structure `T`, a topological space realizer `F`, a set `s` of elements of `α`, and an element `a` of `α`, the set `s` is a neighborhood of `a` (i.e., `s` is in the neighborhood filter of `a`) if and only if there exists an element `b` such that `a` is in the realization of `b` with respect to the functor `F.F` and the realization of `b` with respect to the functor `F.F` is a subset of `s`. In short, this theorem characterizes neighborhoods in terms of a topological space realizer: a set is a neighborhood of a point if and only if it contains the realization of some element with respect to the realizer's functor, and that realization is contained within the set.

More concisely: A set is a neighborhood of a point in a topological space with respect to a given topological space realizer if and only if it contains the realization of some element and is contained in the realization's subset.