Commit 2024-02-05 14:11 2e5d90d5

View on Github →

chore(Topology): move some definitions to new files (#10151) In some cases, the order of implicit arguments changed because now they appear in a different order in variables. Also, some definitions used greek letters for topological spaces, changed to X/Y.

Estimated changes

deleted def AccPt
deleted def ClusterPt
deleted structure Continuous
deleted def ContinuousAt
deleted def Dense
deleted def DenseRange
deleted theorem IsOpen.inter
deleted def IsOpen
deleted def MapClusterPt
deleted def closure
deleted def frontier
deleted def interior
deleted theorem isOpen_sUnion
deleted theorem isOpen_univ
deleted def nhdsWithin
deleted def IsClopen
deleted def Filter.cocompact
deleted def IsCompact
deleted def ContinuousOn
deleted def ContinuousWithinAt
added structure Continuous
added def Dense
added def DenseRange
added def IsClopen
added def IsClosedMap
added theorem IsOpen.inter
added def IsOpen
added def IsOpenMap
added def closure
added def frontier
added def interior
added theorem isOpen_sUnion
added theorem isOpen_univ
added def AccPt
added def ClusterPt
added def ContinuousAt
added def ContinuousOn
added def Filter.cocompact
added def IsCompact
added def MapClusterPt
added def nhdsSet
added def nhdsWithin
added structure ClosedEmbedding
added structure Embedding
added structure Inducing
added structure OpenEmbedding
added def QuotientMap
deleted structure ClosedEmbedding
deleted structure Embedding
deleted structure Inducing
deleted def IsClosedMap
deleted def IsOpenMap
deleted structure OpenEmbedding
deleted def QuotientMap
deleted def nhdsSet