Commit 2024-02-22 12:56 80e03a8b

View on Github →

chore(Topology): move more definitions to Defs (#10623)

Estimated changes

Modified Mathlib/Topology/Defs/Filter.lean

added def Inseparable

added def SeparationQuotient

added def Specializes

added def inseparableSetoid

added def specializationPreorder

Modified Mathlib/Topology/Inseparable.lean

deleted def Inseparable

deleted def SeparationQuotient

deleted def Specializes

deleted def inseparableSetoid

deleted def specializationPreorder