[Merged by Bors] - feat: port Topology.ContinuousFunction.Ideals

[mo271]

---

[mo271]

There was something wrong with the names
WeakDual.characterSpace.continuousMapEval
and
WeakDual.characterSpace.continuousMapEval_apply_apply:

It should have been an upper case "c" in CharacterSpace or one would have to change the name space
In the relevant file, @j-loreaux left the following porting note:

-- porting note: even though the capitalization of the namespace differs, it doesn't matter
-- because there is no dot notation since `characterSpace` is only a type via `CoeSort`.
namespace CharacterSpace
``

Does this mean I should use the namespace "CharacterSpace" here as well and change the name of the theorems starting with `WeakDual.characterSpace` or should I keep my change of the namespace name to "characterSpace", see porting note.
Any thoughts, @j-loreaux ?

[j-loreaux]

@mo271 I wasn't exactly sure about this either, but my feeling is to keep the namespace uppercase (at the very least to be consistent with the previous file, or else change the namespace in that file too). It's possible we'll refactor WeakDual.characterSpace later so that it's actually a subtype, at which point the proper naming will be WeakDual.CharacterSpace anyway, making this a moot point.

Oh, and for clarity: dot notation won't work even if you make this lowercase because all Lean sees for the type is the CoeSort, not characterSpace 𝕜 A itself because that's a term, not a type.

I have addressed a lot of naming issues in this file (sorry, there were a bunch of tricky ones in there!)

[mo271]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234852.20heartbeats.20of.20the.20linter

[mo271]

Regarding the strange time-outs in the linter: Let's try nolint and adidng a porting note

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style