Commit 2024-02-15 16:15 870cb7db

feat: add a TietzeExtension class (#9788) This adds a class TietzeExtension to encode the Tietze extension theorem as a type class that can be satisfied by various types. For now, we provide instances for ℝ, ℝ≥0, ℂ, IsROrC 𝕜, pi types, product types, as well as constructors via homeomorphisms or retracts of a TietzeExtension space, and also a constructor for finite dimensional topological vector spaces.