Theorem Topology.IsGeneratedBy.equiv_symm_comp_continuous_iff

Modification history

2025-10-24 15:50
Mathlib/Topology/Convenient/GeneratedBy.lean
feat(Topology): the topology generated by a family of spaces (#29341) …
Added Topology.IsGeneratedBy.equiv_symm_comp_continuous_iffView on Github →