Theorem TietzeExtension.of_homeo

Modification history

2024-02-15 16:15
Mathlib/Topology/TietzeExtension.lean
feat: add a `TietzeExtension` class (#9788) …
Added TietzeExtension.of_homeoView on Github →