Skip to content

Commit

Permalink
doc(Topology.Category.TopCat.Basic): fix links (#10242)
Browse files Browse the repository at this point in the history
The `trivial` link was linking to Init.Core and `topology.category.TopCat.adjunctions` is from Lean 3 and not valid anymore in Lean 4.
  • Loading branch information
berndlosert committed Feb 6, 2024
1 parent ebb7343 commit ded9c66
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions Mathlib/Topology/Category/TopCat/Basic.lean
Expand Up @@ -13,9 +13,9 @@ import Mathlib.Topology.ContinuousFunction.Basic
# Category instance for topological spaces
We introduce the bundled category `TopCat` of topological spaces together with the functors
`discrete` and `trivial` from the category of types to `TopCat` which equip a type with the
corresponding discrete, resp. trivial, topology. For a proof that these functors are left,
resp. right adjoint to the forgetful functor, see `topology.category.TopCat.adjunctions`.
`TopCat.discrete` and `TopCat.trivial` from the category of types to `TopCat` which equip a type
with the corresponding discrete, resp. trivial, topology. For a proof that these functors are left,
resp. right adjoint to the forgetful functor, see `Mathlib.Topology.Category.TopCat.Adjunctions`.
-/


Expand Down

0 comments on commit ded9c66

Please sign in to comment.