Commit 2025-04-09 06:03 0a57be7c

View on Github →

chore: rename RestrictGenTopology to Topology.IsCoherentWith (#18397) Rename Topology.RestrictGenTopology to Topology.IsCoherentWith since

the Topology part is understood
the name should be prefixed with Is to show it's Prop-valued
"coherent topology" is the informal name for this notion: https://en.wikipedia.org/wiki/Coherent_topology

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Algebra/Module/Alternating/Topology.lean

modified theorem ContinuousAlternatingMap.completeSpace

Modified Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean

modified theorem ContinuousMultilinearMap.completeSpace

Modified Mathlib/Topology/Algebra/Module/StrongTopology.lean

Renamed Mathlib/Topology/RestrictGen.lean to Mathlib/Topology/Coherent.lean

added theorem Topology.IsCoherentWith.isCompact_of_seq

added theorem Topology.IsCoherentWith.isCompact_of_weaklyLocallyCompact

added theorem Topology.IsCoherentWith.of_continuous_prop

added theorem Topology.IsCoherentWith.of_isClosed

added theorem Topology.IsCoherentWith.of_nhds

added theorem Topology.IsCoherentWith.of_seq

deleted theorem Topology.RestrictGenTopology.isCompact_of_seq

deleted theorem Topology.RestrictGenTopology.isCompact_of_weaklyLocallyCompact

deleted theorem Topology.RestrictGenTopology.of_continuous_prop

deleted theorem Topology.RestrictGenTopology.of_isClosed

deleted theorem Topology.RestrictGenTopology.of_nhds

deleted theorem Topology.RestrictGenTopology.of_seq

Modified Mathlib/Topology/Defs/Induced.lean

added structure Topology.IsCoherentWith

deleted structure Topology.RestrictGenTopology

Modified Mathlib/Topology/UniformSpace/CompactConvergence.lean

added theorem ContinuousMap.completeSpace_of_isCoherentWith

deleted theorem ContinuousMap.completeSpace_of_restrictGenTopology

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

modified theorem UniformOnFun.isClosed_setOf_continuous