Frechet Spaces

Stream: Is there code for X?

[Rafael Grenier]

Where in Mathlib are Frechet Spaces?

[Luigi Massacci]

I don't think there's a specific class for it, but we have docs#LocallyConvexSpace and docs#CompleteSpace is already defined in terms of uniformities

[Etienne Marion]

I would say you want to use WithSeminorms with a Countable ι.