feat: port Topology.TietzeExtension (#4246)

Co-authored-by: Komyyy <pol_tta@outlook.jp>
leanprover-community · May 30, 2023 · 8077254 · 8077254
1 parent 4acdb59
commit 8077254
Show file tree

Hide file tree

Showing 2 changed files with 423 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2548,6 +2548,7 @@ import Mathlib.Topology.StoneCech
 import Mathlib.Topology.SubsetProperties
 import Mathlib.Topology.Support
 import Mathlib.Topology.Tactic
+import Mathlib.Topology.TietzeExtension
 import Mathlib.Topology.UniformSpace.AbsoluteValue
 import Mathlib.Topology.UniformSpace.AbstractCompletion
 import Mathlib.Topology.UniformSpace.Basic