# A homeomorphism between finite chain spaces [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-homeomorphism/) 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-homeomorphism-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope Audit a relabeling homeomorphism using every open preimage. Complete finite topologies; no isometry, differentiability or congruence claim. ## Givens and symbols - sets - topology - definition_here - G1 — X={a,b,c}, tau_X={empty,{a},{a,b},X}; Y={u,v,w}, tau_Y={empty,{u},{u,v},Y}. - G2 — h(a)=u,h(b)=v,h(c)=w. - h — relabeling map - k — inverse function ## Rules and sources - mko_definition · cited — Complete source and target finite topologies permit exact audits of every open-set preimage in both directions. Every bijection between finite discrete spaces is a homeomorphism only within that scope. A homeomorphism alone does not establish isometry, differentiability or geometric congruence. · mko-homeomorphism - sets · prerequisite — Compute unions, intersections, complements, inclusion and preimages element by element. - topology · prerequisite — A topology contains empty and whole sets and is closed under arbitrary unions and finite intersections; a finite family admits exhaustive checks. - definition_here · prerequisite — A bijection's inverse has both compositions equal to identities; a homeomorphism is a bijection continuous in both directions, and continuity tests all open preimages. ## Main derivation S01 · impliesBefore \tau_X,\tau_Y\text{ are finite inclusion chains} After \tau_X,\tau_Y\text{ satisfy all topology axioms} Conditions: none Rule: topology · Uses: G1 Leaf basis: topology Each contains both endpoints, and arbitrary unions/finite intersections remain extremal chain members. S02 · impliesBefore h:a\mapsto u,\ b\mapsto v,\ c\mapsto w After h\text{ is total and bijective} Conditions: none Rule: sets · Uses: G1, G2 Leaf basis: sets Each source has one value; the three images are distinct and exhaust Y. S03 · equivalentBefore h^{-1}(\varnothing),\ h^{-1}(\{u\}) After \varnothing,\ \{a\} Conditions: none Rule: sets · Uses: G2 Leaf basis: sets Read the map table to obtain preimages of the first two target opens. S04 · impliesBefore h^{-1}(\{u,v\}),\ h^{-1}(Y) After \{a,b\},\ X Conditions: none Rule: definition_here · Uses: G1, G2, definition_here Leaf basis: definition_here Both remaining preimages lie in tau_X; all four target opens are now checked, so h is continuous. S05 · definitionBefore k=h^{-1} After k(u)=a,\ k(v)=b,\ k(w)=c Conditions: none Rule: definition_here · Uses: S02 Leaf basis: definition_here Construct the inverse entry by entry; both compositions are identities. S06 · impliesBefore k^{-1}(\varnothing),k^{-1}(\{a\}),k^{-1}(\{a,b\}),k^{-1}(X) After \varnothing,\{u\},\{u,v\},Y Conditions: none Rule: definition_here · Uses: G1, S05, definition_here Leaf basis: definition_here Check all four X-opens under k; every preimage is in tau_Y, proving inverse continuity. S07 · definitionBefore h\text{ bijective},\quad h,k\text{ continuous} After h\text{ is a homeomorphism} Conditions: none Rule: definition_here · Uses: S02, S04, S06 Leaf basis: definition_here Only the three established obligations together meet the definition. S08 · impliesBefore A=\{a,b\}\in\tau_X After h(A)=\{u,v\}\in\tau_Y Conditions: none Rule: sets · Uses: G1, S07 Leaf basis: sets Read back one open image as a consistency check; general openness follows from the established inverse continuity. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S08 · premise_audit · G1, S07 — This instance does not replace the complete preimage audit at S06. - S07 · premise_audit · S02, S04, S06 — The conclusion preserves open-set structure and supplies no unspecified distance data. - S06 · premise_audit · G1, S05, definition_here — Inverse continuity was not inferred merely from continuity and bijectivity of h. - S05 · premise_audit · S02 — The established bijectivity licenses this inverse function. - S04 · premise_audit · G1, G2, definition_here — Continuity is a check of every open preimage, not merely point values. - S03 · inverse_equivalence · G2 — These preimages are subsets of X; do not confuse preimage notation with inverse-map direction. - S02 · premise_audit · G1, G2 — Thus the inverse function also has three uniquely specified entries. - S01 · premise_audit · G1 — Both topologies are checked separately, not inferred from equal cardinality. ## Error controls and negative controls Both directionsAudit every open preimage for h and its inverse separately. No structure promotionHomeomorphism does not mean isometry, differentiability or rigid congruence. - Every bijection between equal-cardinality spaces is a homeomorphism. → reject — The identity from a discrete two-point space to an indiscrete one is continuous but its inverse is not. - h is automatically an isometry. → reject — No metrics were given; homeomorphism checks topology only. - Checking only h^{-1}({u}) completes continuity. → reject — Every target open requires checking. ## Result and limitations h is a homeomorphism between the specified finite topologies. ## Verification and source binding 0 declared checks for this guide; only the listed expressions are covered. - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 569c899605b872432df600bc9e60f4e0a755fcd15015d67a2f0f72cb11dbe8dc - original source SHA-256: c108be020f742133584c559dbb70070aa0c7766974d449f9c8a8484a251835dc - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-homeomorphism-01.json)