# Neighborhood: searching for open witnesses and listing all neighborhoods in a four-point topology [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-neighborhood/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-neighborhood-01 · production-20261019-adopted-96 ## 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 S01 · impliesBefore \tau=\{\varnothing,\{1\},\{1,2\},\{3,4\},\{1,3,4\},X\} After (X,\tau)\ \text{is a topological space} Conditions: \tau\ \text{finite} Rule: topology_def · Uses: G1 Leaf basis: topology_def + set_operations_def + nat_induction Confirm the premise: the six members are subsets of X, and ∅, X∈τ. The unions and intersections of the four nontrivial members in pairs are: {1},{1,2} give {1,2} and {1}; {1},{3,4} give {1,3,4} and ∅; {1},{1,3,4} give {1,3,4} and {1}; {1,2},{3,4} give X and ∅; {1,2},{1,3,4} give X and {1}; {3,4},{1,3,4} give {1,3,4} and {3,4}; all are in τ. τ is finite, so every subfamily is finite, and induction on the number of members turns pairwise closure together with ∅, X∈τ into closure under unions of all subfamilies and finite intersections. S02 · equivalentBefore N\in\mathcal{N}(x) After \exists U\in\tau,\ x\in U\ \wedge\ U\subseteq N Conditions: x\in X,\ N\subseteq X Rule: def_unfold · Uses: S01, mko_neighborhood_def Leaf basis: def_unfold + mko_neighborhood_def Unfold the MKO definition: N is a neighborhood of x exactly when some open witness U contains x and is contained in N. τ has only six members, so the existential search is finite: an affirmative answer needs one witness, while a negative answer must rule out all six members (finite_witness_search). S03 · impliesBefore \tau_2=\{U\in\tau\mid 2\in U\} After \tau_2=\{\{1,2\},X\} Conditions: none Rule: set_builder · Uses: G1 Leaf basis: set_builder + finite_witness_search Check each member of τ for the point 2: ∅ no, {1} no, {1,2} yes, {3,4} no, {1,3,4} no, X yes. So the only candidate witnesses for the point 2 are {1,2} and X. S04 · impliesBefore N_1=\{1,2,3\} After U=\{1,2\}:\ 2\in U,\ U\subseteq N_1\ \Rightarrow\ N_1\in\mathcal{N}(2) Conditions: none Rule: exists_intro · Uses: S02, S03, G2 Leaf basis: exists_intro + subset_def Take the witness U={1,2}∈τ: 2∈U, and both elements 1 and 2 of U lie in N1, so U⊆N1. By S02 and ∃-introduction, N1 is a neighborhood of 2. S05 · impliesBefore N_1=\{1,2,3\} After N_1\notin\tau Conditions: none Rule: finite_witness_search · Uses: G1, G2 Leaf basis: finite_witness_search + set_extensionality Compare N1 with each of the six members of τ; none equals {1,2,3}, so N1 is not open. Together with S04: N1 is a neighborhood of 2 but is not open. A neighborhood need not be open. S06 · impliesBefore N_2=\{2,3,4\},\ 2\in N_2 After \{1,2\}\not\subseteq N_2,\ X\not\subseteq N_2\ \Rightarrow\ N_2\notin\mathcal{N}(2) Conditions: none Rule: quantifier_negation · Uses: S02, S03, G2 Leaf basis: quantifier_negation + finite_witness_search + subset_def Although 2∈N2, a witness is still needed. By S03 only {1,2} and X contain 2; both contain 1, and 1∉N2, so neither is contained in N2. The other four open sets do not contain 2 and cannot serve. With no witness, quantifier negation gives that N2 is not a neighborhood of 2. S07 · theorem_applicationBefore O_x=\textstyle\bigcap\{U\in\tau\mid x\in U\} After O_x\in\tau,\ x\in O_x,\ (N\in\mathcal{N}(x)\iff O_x\subseteq N) Conditions: \tau\ \text{finite} Rule: L_least_open · Uses: S01 Leaf basis: topology_def + set_operations_def + subset_def To list all neighborhoods, apply Lemma L_least_open (proved in S07.1 to S07.3): when τ is finite, the intersection O_x of all open sets containing x is itself open and contains x, and N is a neighborhood of x exactly when O_x⊆N. So 'search for a witness' becomes 'check one inclusion'. This least open neighborhood is derived from finiteness; it is not the kind of default that MKO assumption a2 rules out. S08 · impliesBefore O_2=\{1,2\}\cap X After O_2=\{1,2\},\ \mathcal{N}(2)=\{\{1,2\},\{1,2,3\},\{1,2,4\},X\} Conditions: none Rule: L_least_open · Uses: S03, S07 Leaf basis: L_least_open + finite_counting_basics By S03, O_2={1,2}∩X={1,2}. By S07 the neighborhoods of 2 are exactly the subsets containing {1,2}; the elements 3 and 4 may be added freely, giving 2^2=4 sets: {1,2}, {1,2,3}, {1,2,4}, X. This agrees with S04 (N1 contains {1,2}) and S06 (N2 lacks 1). S09 · impliesBefore \tau_1=\{\{1\},\{1,2\},\{1,3,4\},X\} After O_1=\{1\},\ \mathcal{N}(1)=\{N\subseteq X\mid 1\in N\} Conditions: none Rule: L_least_open · Uses: G1, S07 Leaf basis: L_least_open + set_builder + finite_counting_basics The open sets containing 1 are {1}, {1,2}, {1,3,4} and X, with intersection O_1={1}. So the neighborhoods of 1 are exactly the subsets containing 1; each of 2, 3, 4 may be included or not, giving 2^3=8 sets. The point 1 has more neighborhoods than the point 2 because {1} itself is open. S10 · impliesBefore \tau_3=\tau_4=\{\{3,4\},\{1,3,4\},X\} After O_3=O_4=\{3,4\},\ \mathcal{N}(3)=\mathcal{N}(4)=\{\{3,4\},\{1,3,4\},\{2,3,4\},X\} Conditions: none Rule: L_least_open · Uses: G1, S07 Leaf basis: L_least_open + set_builder The open sets containing 3 and those containing 4 form the same family: {3,4}, {1,3,4}, X, with intersection {3,4}. So 3 and 4 have exactly the same 4 neighborhoods. Note that N2={2,3,4} is a neighborhood of 3 and of 4 but not of 2 (S06): whether a set is a neighborhood depends on the point. S11 · theorem_applicationBefore N\in\mathcal{N}(x),\ N\subseteq M\subseteq X After M\in\mathcal{N}(x) Conditions: N\subseteq M\subseteq X Rule: L_upward · Uses: S04 Leaf basis: subset_def + mko_neighborhood_def Apply the upward-closure lemma L_upward (proved in S11.1, valid in every topological space). Example: N1={1,2,3} is a neighborhood of 2 and N1⊆X, so X is a neighborhood of 2 as well, matching the list in S08. S12 · impliesBefore \{2\}\ \text{under}\ \tau\ \text{and under}\ \delta After \{2\}\notin\mathcal{N}_\tau(2),\quad \{2\}\in\mathcal{N}_\delta(2) Conditions: none Rule: mko_neighborhood_def · Uses: G3, S08 Leaf basis: mko_neighborhood_def + exists_intro + quantifier_negation Under τ, O_2={1,2}⊄{2}, so {2} is not a neighborhood of 2 (S08). Under the discrete topology δ, {2}∈δ is itself an open set containing 2 and serves as its own witness, so {2} is a neighborhood of 2. Same underlying set, same point, same candidate, yet the verdict changes with the topology: the list of neighborhoods depends on the topology and the point, not only on the underlying set (MKO paragraph 3). ## Substeps and lemmas S07.1 · impliesBefore \tau_x=\{U\in\tau\mid x\in U\} After O_x\in\tau,\ x\in O_x Conditions: \tau\ \text{finite} Rule: mko_topological_space_def · Uses: mko_topological_space_def, set_operations_def Leaf basis: mko_topological_space_def + set_operations_def τ_x is a subfamily of τ, finite because τ is finite, and nonempty because X∈τ_x. By the axiom on finite intersections, O_x∈τ. Every member of τ_x contains x, so x lies in their intersection. S07.2 · impliesBefore O_x\subseteq N After N\in\mathcal{N}(x) Conditions: none Rule: exists_intro · Uses: S07.1, mko_neighborhood_def Leaf basis: exists_intro + mko_neighborhood_def (⇐) If O_x⊆N, take the witness U=O_x: by S07.1, U∈τ and x∈U, and U⊆N, so N is a neighborhood of x. S07.3 · impliesBefore N\in\mathcal{N}(x) After O_x\subseteq N Conditions: none Rule: exists_elim · Uses: S07.1, mko_neighborhood_def Leaf basis: exists_elim + set_operations_def + subset_def (⇒) If N is a neighborhood of x, take a witness U: U∈τ, x∈U, U⊆N. Then U∈τ_x, and the intersection O_x is contained in each member, so O_x⊆U⊆N. S07.1 to S07.3 together prove L_least_open. S11.1 · impliesBefore x\in U\subseteq N\subseteq M,\ U\in\tau After x\in U\subseteq M\ \Rightarrow\ M\in\mathcal{N}(x) Conditions: none Rule: subset_def · Uses: mko_neighborhood_def, subset_def Leaf basis: subset_def + mko_neighborhood_def + forall_intro Let U be a witness for N. From U⊆N and N⊆M, transitivity of ⊆ gives U⊆M; U is still an open set containing x, so the same U witnesses M, and M is a neighborhood of x. Since x, N and M were arbitrary, this proves L_upward. ## 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 openThe 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 enoughN2={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 factO_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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-neighborhood-01.json)