Theorem WithTopology.topology_eq_coinduced

Modification history

2026-05-19 19:46
Mathlib/Topology/Defs/Induced.lean
feat: define `WithTopology` structure (#39522) …
Added WithTopology.topology_eq_coinducedView on Github →