Commit 2026-05-19 19:46 3db91d81

View on Github →

feat: define WithTopology structure (#39522) WithTopology X t is a 1-field structure wrapper around X with topology coinduced from t. Define the structure, transfer some instances to it, and port CofiniteTopology to use it.

AI usage disclosure

First draft of Topology/WithTopology.lean was written by Gemini.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Compactification/OnePoint/Basic.lean

Modified Mathlib/Topology/Constructions.lean

modified theorem CofiniteTopology.isOpen_iff

modified def CofiniteTopology.of

deleted def CofiniteTopology

Modified Mathlib/Topology/Defs/Basic.lean

added structure WithTopology

Modified Mathlib/Topology/Defs/Induced.lean

added theorem WithTopology.topology_eq_coinduced

Modified Mathlib/Topology/Irreducible.lean

Modified Mathlib/Topology/Order.lean

added theorem WithTopology.topology_eq_induced

added theorem induced_fun_id

Modified Mathlib/Topology/Separation/Basic.lean

Created Mathlib/Topology/WithTopology.lean

added theorem WithTopology.image_ofTopology

added theorem WithTopology.image_toTopology

added theorem WithTopology.ofTopology_bijective

added theorem WithTopology.ofTopology_inj

added theorem WithTopology.ofTopology_injective

added theorem WithTopology.ofTopology_surjective

added theorem WithTopology.ofTopology_toTopology

added theorem WithTopology.preimage_ofTopology

added theorem WithTopology.preimage_toTopology

added theorem WithTopology.toTopology_bijective

added theorem WithTopology.toTopology_inj

added theorem WithTopology.toTopology_injective

added theorem WithTopology.toTopology_ofTopology

added theorem WithTopology.toTopology_surjective