Commit 2026-06-22 16:23 553eb726

chore(Topology): namespace lemmas around IsInducing, IsQuotientMap etc (#40891) The predicates IsInducing, IsEmbedding, IsQuotientMap etc. were moved to the Topology namespace in #15993, but some lemmas were not moved with them, or were added outside of the namespace later. This PR moves these lemmas to the correct namespace to enable dot notation. We do not add deprecation aliases since the lemmas only get namespaced, not renamed, and having both the lemmas and their deprecated aliases available inside the namespace could lead to trouble.