Theorem Topology.IsCoherentWith.isCompact_of_seq

Modification history

2025-06-03 15:37

Mathlib/Topology/Coherent.lean

feat: a weaker definition of compactly generated spaces (#21237) …

Deleted Topology.IsCoherentWith.isCompact_of_seq View on Github →

2025-04-09 06:03

Mathlib/Topology/Coherent.lean

chore: rename `RestrictGenTopology` to `Topology.IsCoherentWith` (#18397) …

Added Topology.IsCoherentWith.isCompact_of_seq View on Github →