Theorem ContinuousMap.exists_extension'

Modification history

2024-08-07 07:08

Mathlib/Topology/TietzeExtension.lean

chore: backports for leanprover/lean4#4814 (part 22) (#15511)

Modified ContinuousMap.exists_extension'View on Github →

2024-02-15 16:15

Mathlib/Topology/TietzeExtension.lean

feat: add a `TietzeExtension` class (#9788) …

Added ContinuousMap.exists_extension'View on Github →