new name for Cauchy

Stream: mathlib4

[Rémy Degenne]

In mathlib3 we had a property cauchy f for a filter f and then we used the name Cauchy α for { f : filter α // cauchy f }. Now in mathlib4, the property is called Cauchy . What name should we give to { f : Filter α // Cauchy f } ?
That questions comes from PR !4#2269

[Reid Barton]

CauchyCat, obviously :meow:

[Reid Barton]

CauchyFilter?

[Reid Barton]

CompletionButNotSeparated?

[Reid Barton]

Does Bourbaki name it? or proceed directly to the completion

[Johan Commelin]

How about Cauchy ↦ Filter.Cauchy so that this subtype can remain _root_.Cauchy?

[Rémy Degenne]

It looks like the subtype is not used beyond that file, so it may be easier to change that, and leave the filter property as it is.
CauchyFilter could work.

[Rémy Degenne]

Or, since the docstring of the file calls that object the uniform completion of the space, we could use UniformCompletion

[Rémy Degenne]

I went with CauchyFilter and updated the PR

[Yaël Dillies]

Why not rename Cauchy to IsCauchy?

[Johan Commelin]

@Rémy Degenne would you mind updating the module docstring so that it no longer mentions coe?

[Rémy Degenne]

I suppose I can do that, but I don't really see what I should replace it with. CoeTC.coe? Or somehow remove coe completely, and do something else?
At this point, my comprehension of lean 4 is very rudimentary and my limited porting experience is mostly to shake the code a bit till the squiggly lines disappear.

[Johan Commelin]

I think that the "standard" way to talk about coe in Lean 4 is to write (\u) where \u is the up-arrow.

[Patrick Massot]

The subtype has indeed very limited use as an intermediate step in the completion construction. Bourbaki does completion slightly differently, using the subtype of minimal Cauchy filters instead of quotienting the subtype of all Cauchy filters like we do.