Commit 2024-09-05 13:49 e02e60ee

View on Github →

refactor(Topology/Group): reorganize section about quotient groups (#15529)

  • move TopologicalGroup.exists_antitone_basis_nhds_one up out of the section about quotient groups;
  • use namespace QuotientGroup;
  • rename topologicalGroup_quotient to QuotientGroup.instTopologicalGroup, turn the old name into a deprecated alias;
  • generalize QuotientGroup.nhds_one_isCountablyGenerated to QuotientGroup.instFirstCountableTopology.

Estimated changes

modified theorem QuotientGroup.isOpenMap_coe
modified theorem QuotientGroup.nhds_eq