Neighborhood: searching for open witnesses and listing all neighborhoods in a four-point topology

Goal and scope

Let X={1,2,3,4} and τ={∅,{1},{1,2},{3,4},{1,3,4},X}. Decide whether N1={1,2,3} and N2={2,3,4} are neighborhoods of the point 2; prove that in a finite topology the neighborhoods of x are exactly the subsets containing O_x (the intersection of all open sets containing x), and use this to list all neighborhoods of the points 1, 2, 3 and 4; prove that neighborhoods are closed upwards; and show that the verdict for the same set can change under the discrete topology.

Works inside the MKO's scope: X, τ, the point and the candidate sets are explicit (assumption a1), and a neighborhood means a set containing an open set that contains the point, with no distance, radius or assumed least neighborhood (assumption a2); the least neighborhood O_x in this example is derived from τ being finite, not assumed. It does not formalize the neighborhood filter and does not change the canonical MKO or its English edition.

Givens and symbols

• subset_def
• set_operations_def
• finite_counting_basics
• nat_induction

• G1 — The underlying set X={1,2,3,4} and the topology τ={∅,{1},{1,2},{3,4},{1,3,4},X} (MKO assumption a1).
• G2 — Candidate point and sets: x=2, N1={1,2,3}, N2={2,3,4}; all satisfy x∈X and N⊆X.
• G3 — For comparison, the discrete topology δ=P(X), in which every subset of X is open.

• X — the underlying set {1,2,3,4}
• \tau — the topology on X
• \tau_x — the family of open sets containing x, {U∈τ ∣ x∈U}
• O_x — the intersection of all members of τ_x
• \mathcal{N}(x) — all neighborhoods of x
• \delta — the discrete topology P(X) on X

Rules and sources

• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
• finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
• nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
• topology_def · prerequisite — Topology: a family τ of open subsets of X containing ∅ and X, closed under arbitrary unions and finite intersections.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• exists_elim · prerequisite — ∃-elimination: from ∃x∈D, P(x) we may name some element a with P(a) by a fresh name; reasoning with a is allowed as long as the final conclusion does not mention a.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• mko_neighborhood_def · cited — In a topological space (X,τ), N⊆X is a neighborhood of x∈X exactly when there is U∈τ with x∈U⊆N. The open sets containing x form an open neighborhood base, but a general neighborhood need not itself be open. · mko-neighborhood
• mko_topological_space_def · cited — A topology on X is a family τ⊆P(X) with ∅∈τ, X∈τ, unions of all subfamilies in τ, and intersections of all finite subfamilies in τ (the empty intersection read as X). · mko-topological-space
• finite_witness_search · prerequisite — For an explicitly listed finite set F, ∃U∈F, Q(U) is equivalent to Q holding for some listed member; to refute it, every member of F must be checked and found not to satisfy Q.
• L_least_open · lemma — Let (X,τ) be a topological space with τ finite, x∈X, and O_x=∩{U∈τ ∣ x∈U}. Then O_x∈τ, x∈O_x, and for every N⊆X: N is a neighborhood of x exactly when O_x⊆N.
• L_upward · lemma — In any topological space, if N is a neighborhood of x and N⊆M⊆X, then M is also a neighborhood of x.

Main derivation

\tau=\{\varnothing,\{1\},\{1,2\},\{3,4\},\{1,3,4\},X\}

(X,\tau)\ \text{is a topological space}

N\in\mathcal{N}(x)

\exists U\in\tau,\ x\in U\ \wedge\ U\subseteq N

\tau_2=\{U\in\tau\mid 2\in U\}

\tau_2=\{\{1,2\},X\}

N_1=\{1,2,3\}

U=\{1,2\}:\ 2\in U,\ U\subseteq N_1\ \Rightarrow\ N_1\in\mathcal{N}(2)

N_1=\{1,2,3\}

N_1\notin\tau

N_2=\{2,3,4\},\ 2\in N_2

\{1,2\}\not\subseteq N_2,\ X\not\subseteq N_2\ \Rightarrow\ N_2\notin\mathcal{N}(2)

O_x=\textstyle\bigcap\{U\in\tau\mid x\in U\}

O_x\in\tau,\ x\in O_x,\ (N\in\mathcal{N}(x)\iff O_x\subseteq N)

O_2=\{1,2\}\cap X

O_2=\{1,2\},\ \mathcal{N}(2)=\{\{1,2\},\{1,2,3\},\{1,2,4\},X\}

\tau_1=\{\{1\},\{1,2\},\{1,3,4\},X\}

O_1=\{1\},\ \mathcal{N}(1)=\{N\subseteq X\mid 1\in N\}

\tau_3=\tau_4=\{\{3,4\},\{1,3,4\},X\}

O_3=O_4=\{3,4\},\ \mathcal{N}(3)=\mathcal{N}(4)=\{\{3,4\},\{1,3,4\},\{2,3,4\},X\}

N\in\mathcal{N}(x),\ N\subseteq M\subseteq X

M\in\mathcal{N}(x)

\{2\}\ \text{under}\ \tau\ \text{and under}\ \delta

\{2\}\notin\mathcal{N}_\tau(2),\quad \{2\}\in\mathcal{N}_\delta(2)

Substeps and lemmas

\tau_x=\{U\in\tau\mid x\in U\}

O_x\in\tau,\ x\in O_x

O_x\subseteq N

N\in\mathcal{N}(x)

N\in\mathcal{N}(x)

O_x\subseteq N

x\in U\subseteq N\subseteq M,\ U\in\tau

x\in U\subseteq M\ \Rightarrow\ M\in\mathcal{N}(x)

Reverse audits

• S12 · premise_audit · G3, S08, mko_neighborhood_def — Each verdict uses only the definition with the corresponding topology; nothing else about δ is claimed.
• S11.1 · premise_audit · mko_neighborhood_def, subset_def, forall_intro — Only the definition and transitivity of inclusion are used, not the finiteness of τ, so it holds in every topological space.
• S11 · premise_audit · L_upward, S04 — Upward closure does not give downward closure: {1,2} is a neighborhood of 2, but its subset {2} is not.
• S10 · premise_audit · G1, S07 — τ_3 and τ_4 both come from checking all six members (N5 records the size 3).
• S09 · premise_audit · G1, S07, finite_counting_basics — τ_1 comes from checking all six members (N4 records its size 4); the count is N3.
• S08 · premise_audit · S03, S07, finite_counting_basics — Completeness of the list comes from the two-way equivalence in the lemma and the subset count (N2).
• S07.3 · premise_audit · S07.1, exists_elim, subset_def — It uses that an intersection is contained in each member and that ⊆ is transitive; the conclusion does not mention the witness U, as ∃-elimination requires.
• S07.2 · premise_audit · S07.1, mko_neighborhood_def, exists_intro — The witness O_x must be open, which is exactly what S07.1 provides.
• S07.1 · premise_audit · mko_topological_space_def, set_operations_def — The key is the finite intersection axiom; if τ_x were infinite, the intersection need not be open.
• S07 · premise_audit · L_least_open, S01 — The lemma needs τ finite; in the usual topology of ℝ, the intersection of the open sets containing 0 is {0}, which is not open, and 0 has no least neighborhood (see error control three).
• S06 · premise_audit · S03, quantifier_negation, finite_witness_search — Refuting the existential requires excluding all six members: four because they miss 2, two because they are not contained in N2.
• S05 · premise_audit · G1, finite_witness_search — 'Not open' requires comparing with all six members.
• S04 · premise_audit · S02, S03, exists_intro, subset_def — One witness suffices; the witness must be a member of τ, not just any set containing 2.
• S03 · premise_audit · G1, set_builder, finite_witness_search — All six members are checked, so the list τ_2 is complete (N1 records its size 2).
• S02 · inverse_equivalence · mko_neighborhood_def, def_unfold — Unfolding and folding the definition are inverse moves. Note there are two conditions, x∈U and U⊆N; x∈N alone is not enough.
• S01 · premise_audit · G1, topology_def, mko_topological_space_def, nat_induction — It needs the complete pairwise check and τ finite; if τ were not a topology, the definition of neighborhood would not apply.

Error controls and negative controls

A neighborhood need not be open

The misconception identified in the MKO is identifying neighborhoods with open sets or open balls. N1={1,2,3} is not in τ, yet it is a neighborhood of 2 because it contains the open set {1,2}∋2 (S04, S05). The definition only requires containing an open set that contains the point.

Checking x∈N is not enough

N2={2,3,4} contains 2, but the open sets containing 2, {1,2} and X, both contain 1 and do not fit inside N2 (S06). Deciding a neighborhood requires a search for an open witness, and a negative answer must exclude every candidate.

The least neighborhood comes from finiteness, not from a general fact

O_x in S07 is open because τ is finite and the intersection is finite. In the usual topology of ℝ, if N were a least neighborhood of 0 it would lie inside every interval (−1/n,1/n) indexed by positive integers n≥1, so by the Archimedean property N⊆{0}, i.e. N={0}; but {0} contains no open interval around 0 and is not a neighborhood of 0, a contradiction. So 0 has no least neighborhood, and the method of this example may not be turned into a general assumption (MKO assumption a2).

• {1,2,3} is not open, so it is not a neighborhood of the point 2 → reject — The witness {1,2}∈τ satisfies 2∈{1,2}⊆{1,2,3}.
• 2∈{2,3,4}, so {2,3,4} is a neighborhood of the point 2 → reject — The only open sets containing 2 are {1,2} and X, both containing 1∉{2,3,4}, so there is no witness.
• The singleton {2} is always a neighborhood of the point 2 → reject — Under τ, O_2={1,2}⊄{2}; it holds only in topologies such as the discrete one where {2} is open.
• 3 and 4 are different points, so their families of neighborhoods must differ → reject — O_3=O_4={3,4}, so the two points have exactly the same neighborhoods (S10).

Result and limitations

N1={1,2,3} is a neighborhood of the point 2 (witness {1,2}) but is not open; N2={2,3,4} contains 2 but is not a neighborhood of 2. In a finite topology N is a neighborhood of x exactly when O_x⊆N; here O_1={1}, O_2={1,2}, O_3=O_4={3,4}, so 1 has 8 neighborhoods, 2 has 4, and 3 and 4 share the same 4. Neighborhoods are closed upwards; under the discrete topology {2} is a neighborhood of 2, under τ it is not.

• The binding to Mathlib's nhds, nhds_basis_opens and the upward-closed neighborhood filter (MKO formal next) is not built here.

Verification and source binding

5 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: a79028f77322db110cfe9e06c126ca7f2fafe3f16ff676c8b59b56e6bad4389a
• original source SHA-256: b21c0ed8194f848c969d43585bab34a26ff70a3a4c37bb4e3de7b9931a5e0ef4
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)