feat: define WithTopology structure (leanprover-community#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.

Author: urkud

Mathlib.lean

@@ -8038,6 +8038,7 @@ public import Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
 public import Mathlib.Topology.VectorBundle.FiniteDimensional
 public import Mathlib.Topology.VectorBundle.Hom
 public import Mathlib.Topology.VectorBundle.Riemannian
+public import Mathlib.Topology.WithTopology
 public import Mathlib.Util.AddRelatedDecl
 public import Mathlib.Util.AliasIn
 public import Mathlib.Util.AssertNoSorry

Mathlib/Topology/Compactification/OnePoint/Basic.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Data.Fintype.Option
 public import Mathlib.Topology.Homeomorph.Lemmas
 public import Mathlib.Topology.Sets.Opens
+import Mathlib.Topology.WithTopology
 
 /-!
 # The one-point compactification
@@ -550,8 +551,8 @@ theorem not_continuous_cofiniteTopology_of_symm [Infinite X] [DiscreteTopology X
   inhabit X
   simp only [continuous_iff_continuousAt, ContinuousAt, not_forall]
   use CofiniteTopology.of ↑(default : X)
-  simpa [nhds_coe_eq, nhds_discrete, CofiniteTopology.nhds_eq] using
-    (finite_singleton ((default : X) : OnePoint X)).infinite_compl
+  simpa [nhds_coe_eq, nhds_discrete, CofiniteTopology.nhds_eq, Equiv.symm_apply_eq]
+    using (finite_singleton _).infinite_compl
 
 instance (X : Type*) [TopologicalSpace X] [DiscreteTopology X] :
     TotallySeparatedSpace (OnePoint X) where

Mathlib/Topology/Constructions.lean

@@ -13,6 +13,7 @@ public import Mathlib.Order.Filter.Cofinite
 public import Mathlib.Order.Filter.Curry
 public import Mathlib.Topology.Constructions.SumProd
 public import Mathlib.Topology.NhdsSet
+import Mathlib.Topology.WithTopology
 
 /-!
 # Constructions of new topological spaces from old ones
@@ -272,19 +273,9 @@ lemma DiscreteTopology.isDiscrete [DiscreteTopology s] : IsDiscrete s := ⟨infe
 
 end IsDiscrete
 
-/-- A type synonym equipped with the topology whose open sets are the empty set and the sets with
-finite complements. -/
-def CofiniteTopology (X : Type*) := X
-
-namespace CofiniteTopology
-
-/-- The identity equivalence between `X` and `CofiniteTopology X`. -/
-def of : X ≃ CofiniteTopology X :=
-  Equiv.refl X
-
-instance [Inhabited X] : Inhabited (CofiniteTopology X) where default := of default
-
-instance : TopologicalSpace (CofiniteTopology X) where
+/-- Cofinite topology. A set is open if it's empty or cofinite. -/
+@[implicit_reducible]
+protected def TopologicalSpace.cofinite {X : Type*} : TopologicalSpace X where
   IsOpen s := s.Nonempty → Set.Finite sᶜ
   isOpen_univ := by simp
   isOpen_inter s t := by
@@ -296,8 +287,22 @@ instance : TopologicalSpace (CofiniteTopology X) where
     rw [compl_sUnion]
     exact Finite.sInter (mem_image_of_mem _ hts) (h t hts ⟨x, hzt⟩)
 
-theorem isOpen_iff {s : Set (CofiniteTopology X)} : IsOpen s ↔ s.Nonempty → sᶜ.Finite :=
-  Iff.rfl
+/-- A type synonym equipped with the topology whose open sets are the empty set and the sets with
+finite complements. -/
+abbrev CofiniteTopology (X : Type*) :=
+  WithTopology X .cofinite
+
+namespace CofiniteTopology
+
+/-- The identity equivalence between `X` and `CofiniteTopology X`. -/
+def of : X ≃ CofiniteTopology X := (WithTopology.equiv _ _).symm
+
+instance [Inhabited X] : Inhabited (CofiniteTopology X) where default := of default
+
+theorem isOpen_iff {s : Set (CofiniteTopology X)} : IsOpen s ↔ s.Nonempty → sᶜ.Finite := by
+  simp_rw [isOpen_coinduced, TopologicalSpace.cofinite, isOpen_mk, ← Set.preimage_compl,
+    WithTopology.preimage_toTopology, image_nonempty,
+    finite_image_iff (WithTopology.ofTopology_injective _).injOn]
 
 theorem isOpen_iff' {s : Set (CofiniteTopology X)} : IsOpen s ↔ s = ∅ ∨ sᶜ.Finite := by
   simp only [isOpen_iff, nonempty_iff_ne_empty, or_iff_not_imp_left]
@@ -307,7 +312,7 @@ theorem isClosed_iff {s : Set (CofiniteTopology X)} : IsClosed s ↔ s = univ 
 
 theorem nhds_eq (x : CofiniteTopology X) : 𝓝 x = pure x ⊔ cofinite := by
   ext U
-  rw [mem_nhds_iff]
+  simp_rw [mem_nhds_iff, isOpen_iff]
   constructor
   · rintro ⟨V, hVU, V_op, haV⟩
     exact mem_sup.mpr ⟨hVU haV, mem_of_superset (V_op ⟨_, haV⟩) hVU⟩

Mathlib/Topology/Defs/Basic.lean

@@ -227,3 +227,22 @@ Formulated here when the source space is ℕ.
 Use `dense_iInter_of_isOpen` which works for any countable index type instead. -/
 class BaireSpace (X : Type*) [TopologicalSpace X] : Prop where
   baire_property : ∀ f : ℕ → Set X, (∀ n, IsOpen (f n)) → (∀ n, Dense (f n)) → Dense (⋂ n, f n)
+
+/-- A one-field structure wrapper for `X` with the topology coinduced from `t`. -/
+@[ext]
+structure WithTopology (X : Type*) (t : TopologicalSpace X) where
+  /-- Converts an element of `X` to an element of `WithTopology X t`. -/
+  toTopology (t) ::
+  /-- Converts an element of `WithTopology X t` to an element of `X`. -/
+  ofTopology : X
+
+section Notation
+
+open Lean.PrettyPrinter.Delaborator
+
+/-- This prevents `toTopology t x` being printed as `{ ofTopology := x }`
+by `delabStructureInstance`. -/
+@[app_delab WithTopology.toTopology]
+meta def WithTopology.delabToTopology : Delab := delabApp
+
+end Notation

Mathlib/Topology/Defs/Induced.lean

@@ -90,6 +90,26 @@ def coinduced (f : X → Y) (t : TopologicalSpace X) : TopologicalSpace Y where
 
 end TopologicalSpace
 
+namespace WithTopology
+
+instance instTopologicalSpace (X : Type*) (t : TopologicalSpace X) :
+    TopologicalSpace (WithTopology X t) :=
+  .coinduced (WithTopology.toTopology t) t
+
+lemma topology_eq_coinduced (X : Type*) (t : TopologicalSpace X) :
+    instTopologicalSpace X t = .coinduced (.toTopology t) t :=
+  rfl
+
+/-- `WithTopology.ofTopology` and `WithTopology.toTopology` as an equivalence. -/
+@[simps]
+protected def equiv (X : Type*) (t : TopologicalSpace X) : WithTopology X t ≃ X where
+  toFun := WithTopology.ofTopology
+  invFun := WithTopology.toTopology t
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+end WithTopology
+
 namespace Topology
 variable {X Y : Type*} [tX : TopologicalSpace X] [tY : TopologicalSpace Y]
 

Mathlib/Topology/Irreducible.lean

@@ -10,6 +10,7 @@ public import Mathlib.Order.Zorn
 public import Mathlib.Topology.ContinuousOn
 public import Mathlib.Topology.DiscreteSubset
 public import Mathlib.Tactic.CrossRefAttribute
+import Mathlib.Topology.WithTopology
 
 /-!
 # Irreducibility in topological spaces
@@ -264,11 +265,10 @@ instance (priority := 100) [IndiscreteTopology X] : PreirreducibleSpace X where
 /-- An infinite type with cofinite topology is an irreducible topological space. -/
 instance (priority := 100) {X} [Infinite X] : IrreducibleSpace (CofiniteTopology X) where
   isPreirreducible_univ u v := by
-    haveI : Infinite (CofiniteTopology X) := ‹_›
     simp only [CofiniteTopology.isOpen_iff, univ_inter]
     intro hu hv hu' hv'
     simpa only [compl_union, compl_compl] using ((hu hu').union (hv hv')).infinite_compl.nonempty
-  toNonempty := (inferInstance : Nonempty X)
+  toNonempty := inferInstance
 
 theorem irreducibleComponents_eq_singleton [IrreducibleSpace X] :
     irreducibleComponents X = {univ} :=

Mathlib/Topology/Order.lean

@@ -489,6 +489,8 @@ theorem induced_id [t : TopologicalSpace α] : t.induced id = t :=
   TopologicalSpace.ext <|
     funext fun s => propext <| ⟨fun ⟨_, hs, h⟩ => h ▸ hs, fun hs => ⟨s, hs, rfl⟩⟩
 
+theorem induced_fun_id {t : TopologicalSpace α} : t.induced (·) = t := induced_id
+
 theorem induced_compose {tγ : TopologicalSpace γ} {f : α → β} {g : β → γ} :
     (tγ.induced g).induced f = tγ.induced (g ∘ f) :=
   TopologicalSpace.ext <|
@@ -516,6 +518,10 @@ theorem Equiv.coinduced_symm {α β : Type*} (e : α ≃ β) :
     TopologicalSpace.coinduced e.symm = TopologicalSpace.induced e :=
   e.symm.induced_symm.symm
 
+lemma WithTopology.topology_eq_induced {X : Type*} (t : TopologicalSpace X) :
+    instTopologicalSpace X t = .induced ofTopology t :=
+  congrFun (WithTopology.equiv X t).coinduced_symm t
+
 end GaloisConnection
 
 -- constructions using the complete lattice structure
@@ -570,6 +576,20 @@ instance : DiscreteTopology ℤ := ⟨rfl⟩
 instance {n} : TopologicalSpace (Fin n) := ⊥
 instance {n} : DiscreteTopology (Fin n) := ⟨rfl⟩
 
+instance : DiscreteTopology (WithTopology α ⊥) where
+  eq_bot := coinduced_bot
+
+instance : IndiscreteTopology (WithTopology α ⊤) where
+  eq_top := by rw [WithTopology.topology_eq_induced, induced_top]
+
+protected theorem WithTopology.nontrivialTopology_iff {t : TopologicalSpace α} :
+    NontrivialTopology (WithTopology α t) ↔ t ≠ ⊤ := by
+  simp_rw [nontrivialTopology_iff, topology_eq_induced, ne_eq, not_iff_not]
+  constructor
+  · intro h
+    simpa [induced_compose, comp_def, induced_fun_id] using congr(induced (toTopology t) $h)
+  · simp +contextual
+
 lemma Nat.cast_continuous {R : Type*} [NatCast R] [TopologicalSpace R] :
     Continuous (Nat.cast (R := R)) :=
   continuous_of_discreteTopology

Mathlib/Topology/Separation/Basic.lean

@@ -392,6 +392,9 @@ theorem TopologicalSpace.IsTopologicalBasis.exists_mem_of_ne [T1Space X] {b : Se
 protected theorem Finset.isClosed [T1Space X] (s : Finset X) : IsClosed (s : Set X) :=
   s.finite_toSet.isClosed
 
+instance : T1Space (CofiniteTopology X) where
+  t1 x := CofiniteTopology.isClosed_iff.mpr <| by simp
+
 theorem t1Space_TFAE (X : Type u) [TopologicalSpace X] :
     List.TFAE [T1Space X,
       ∀ x, IsClosed ({ x } : Set X),
@@ -421,9 +424,13 @@ theorem t1Space_TFAE (X : Type u) [TopologicalSpace X] :
   tfae_have 1 → 4 := by
     simp only [continuous_def, CofiniteTopology.isOpen_iff']
     rintro H s (rfl | hs)
-    exacts [isOpen_empty, compl_compl s ▸ (@Set.Finite.isClosed _ _ H _ hs).isOpen_compl]
-  tfae_have 4 → 2 :=
-    fun h x => (CofiniteTopology.isClosed_iff.2 <| Or.inr (finite_singleton _)).preimage h
+    · exact isOpen_empty
+    · rw [← compl_compl s, preimage_compl]
+      exact hs.preimage (Equiv.injective _).injOn |>.isClosed.isOpen_compl
+  tfae_have 4 → 2 := by
+    intro h x
+    rw [← CofiniteTopology.of.preimage_image {x}]
+    exact (Set.Finite.isClosed <| by simp) |>.preimage h
   tfae_have 2 ↔ 10 := by
     simp only [← closure_subset_iff_isClosed, specializes_iff_mem_closure, subset_def,
       mem_singleton_iff, eq_comm]
@@ -480,9 +487,6 @@ theorem nhds_le_nhds_iff [T1Space X] {a b : X} : 𝓝 a ≤ 𝓝 b ↔ a = b :=
 instance (priority := 100) [T1Space X] : R0Space X :=
   (t1Space_iff_t0Space_and_r0Space.mp ‹T1Space X›).right
 
-instance : T1Space (CofiniteTopology X) :=
-  t1Space_iff_continuous_cofinite_of.mpr continuous_id
-
 instance (priority := 80) [T0Space X] [R0Space X] : T1Space X :=
   t1Space_iff_t0Space_and_r0Space.mpr ⟨‹T0Space X›, ‹R0Space X›⟩
 

Mathlib/Topology/WithTopology.lean

@@ -0,0 +1,147 @@
+/-
+Copyright (c) 2026 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov, Gemini CLI
+-/
+module
+
+public import Mathlib.Topology.Defs.Induced
+
+/-!
+# Basic lemmas and instances about the `WithTopology` type synonym
+
+`WithTopology X t` is a copy of `X` equipped with the topology `t`.
+This is useful for providing multiple topologies on the same type
+without causing instance conflicts.
+
+In this file we setup basic API about this type
+and transfer instances (basic, order) from `X` to `WithTopology X t`.
+
+## Implementation notes
+
+The pattern here is the same one as is used by `Lex` for order structures
+and `WithLp` for metric structures.
+-/
+
+public section
+
+variable {X : Type*} (t : TopologicalSpace X)
+
+namespace WithTopology
+
+lemma ofTopology_toTopology (x : X) : ofTopology (toTopology t x) = x := rfl
+
+@[simp]
+lemma toTopology_ofTopology (x : WithTopology X t) :
+  toTopology t (ofTopology x) = x := rfl
+
+lemma ofTopology_surjective : Function.Surjective (ofTopology (t := t)) :=
+  Function.RightInverse.surjective <| ofTopology_toTopology _
+
+lemma toTopology_surjective : Function.Surjective (toTopology t) :=
+  Function.RightInverse.surjective <| toTopology_ofTopology _
+
+lemma ofTopology_injective : Function.Injective (ofTopology (t := t)) :=
+  Function.LeftInverse.injective <| toTopology_ofTopology _
+
+lemma toTopology_injective : Function.Injective (toTopology t) :=
+  Function.LeftInverse.injective <| ofTopology_toTopology _
+
+lemma ofTopology_bijective : Function.Bijective (ofTopology (t := t)) :=
+  ⟨ofTopology_injective t, ofTopology_surjective t⟩
+
+lemma toTopology_bijective : Function.Bijective (toTopology t) :=
+  ⟨toTopology_injective t, toTopology_surjective t⟩
+
+/-- Injectivity lemma for the constructor `toTopology t`.
+
+It is not marked as `@[simp]`, because its autogenerated version
+is already in the default `simp` set. -/
+lemma toTopology_inj {x y : X} : toTopology t x = toTopology t y ↔ x = y :=
+  (toTopology_injective t).eq_iff
+
+@[simp] lemma ofTopology_inj {x y : WithTopology X t} : ofTopology x = ofTopology y ↔ x = y :=
+  (ofTopology_injective t).eq_iff
+
+/-! ### Set-theoretic lemmas -/
+
+open Set
+
+lemma image_ofTopology (s : Set (WithTopology X t)) : ofTopology '' s = toTopology t ⁻¹' s :=
+  WithTopology.equiv X t |>.symm.image_symm_eq_preimage _
+
+lemma preimage_toTopology (s : Set (WithTopology X t)) : toTopology t ⁻¹' s = ofTopology '' s :=
+  (image_ofTopology t s).symm
+
+lemma image_toTopology (s : Set X) : toTopology t '' s = ofTopology ⁻¹' s :=
+  WithTopology.equiv X t |>.symm.image_eq_preimage_symm _
+
+lemma preimage_ofTopology (s : Set X) : ofTopology ⁻¹' s = toTopology t '' s :=
+  (image_toTopology t s).symm
+
+/-!
+### Instance transfers
+
+In this section we transfer some instances from `X` to `WithTopology X t`.
+-/
+
+instance [Nonempty X] : Nonempty (WithTopology X t) :=
+  (WithTopology.equiv X t).nonempty
+
+instance [Inhabited X] : Inhabited (WithTopology X t) :=
+  ⟨toTopology t default⟩
+
+instance [Subsingleton X] : Subsingleton (WithTopology X t) :=
+  (WithTopology.equiv X t).subsingleton
+
+instance [Unique X] : Unique (WithTopology X t) := .mk' _
+
+instance [Finite X] : Finite (WithTopology X t) := .of_equiv _ (WithTopology.equiv X t).symm
+
+instance [Infinite X] : Infinite (WithTopology X t) := .of_injective _ <| toTopology_injective _
+
+instance [Fintype X] : Fintype (WithTopology X t) :=
+  .ofBijective (.toTopology t) (toTopology_bijective t)
+
+deriving instance DecidableEq for WithTopology
+
+instance [LE X] : LE (WithTopology X t) where
+  le x y := ofTopology x ≤ ofTopology y
+
+instance [LT X] : LT (WithTopology X t) where
+  lt x y := ofTopology x < ofTopology y
+
+-- TODO: `inferInstance` works here, but it shouldn't
+instance [LE X] [DecidableLE X] : DecidableLE (WithTopology X t) := fun x y ↦
+  inferInstanceAs (Decidable (x.ofTopology ≤ y.ofTopology))
+
+-- TODO: `inferInstance` works here, but it shouldn't
+instance [LT X] [DecidableLT X] : DecidableLT (WithTopology X t) := fun x y ↦
+  inferInstanceAs (Decidable (x.ofTopology < y.ofTopology))
+
+instance [Preorder X] : Preorder (WithTopology X t) :=
+  .lift ofTopology
+
+instance [PartialOrder X] : PartialOrder (WithTopology X t) :=
+  ofTopology_injective t |>.partialOrder _ .rfl .rfl
+
+@[to_dual]
+instance [Max X] : Max (WithTopology X t) where
+  max x y := toTopology t (max x.ofTopology y.ofTopology)
+
+@[to_dual]
+instance [SemilatticeSup X] : SemilatticeSup (WithTopology X t) :=
+  ofTopology_injective t |>.semilatticeSup _ .rfl .rfl fun _ _ ↦ rfl
+
+instance [Lattice X] : Lattice (WithTopology X t) where
+
+instance [DistribLattice X] : DistribLattice (WithTopology X t) where
+  le_sup_inf _ _ _ := le_sup_inf (α := X)
+
+instance [Ord X] : Ord (WithTopology X t) where
+  compare x y := compare x.ofTopology y.ofTopology
+
+instance [LinearOrder X] : LinearOrder (WithTopology X t) :=
+  ofTopology_injective t |>.linearOrder _ .rfl .rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
+
+end WithTopology