Theorem TietzeExtension.of_retract

Modification history

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