Def compactumToCompHaus.full

Modification history

2024-04-27 09:23

Mathlib/Topology/Category/Compactum.lean

chore(CategoryTheory): make `Functor.Full` a Prop (#12449) …

Deleted compactumToCompHaus.full View on Github →

2024-04-12 14:33

Mathlib/Topology/Category/Compactum.lean

chore(CategoryTheory): move Full, Faithful, EssSurj, IsEquivalence and ReflectsIsomorphisms to the Functor namespace (#11985) …

Modified compactumToCompHaus.full View on Github →

2023-06-08 04:21

Mathlib/Topology/Category/Compactum.lean

feat: port Topology.Category.Compactum (#3872)

Added compactumToCompHaus.full View on Github →