[Merged by Bors] - feat: add a TietzeExtension class

[j-loreaux]

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.

---

[ADedecker]

I'll give this a deeper look soon, but a first comment:

note: we'll leave IsROrC 𝕜 for a future PR because this is a rare case where we're going to do things backwards and prove it first for ℝ and ℂ, and then use those for the IsROrC version.

Why not provide an instance/reducible-def for finite dimensional T2 real TVS, by reducing it to products using LinearEquiv.toContinuousLinearEquiv. Then it will apply directly to IsROrC, right?

[j-loreaux]

@ADedecker I've implemented your nice suggestion. It can't be an instance because there is no way for Lean to know which scalar field is intended, so it's just a theorem.

Optionally, I could provide in additional an actual instance, where the scalar field is just assumed to be IsROrC. This would allow us to get TietzeExtension (EuclideanSpace 𝕜 n) for free. (EDIT: I've added this instance)

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style