Renaming `norm_eq_zero` to `norm_eq_zero_iff`

Stream: mathlib4

[Eric Wieser]

I want to claim this name for the theorem that says "in a trivial topological space, the norm is always zero", that is

theorem norm_eq_zero [SomeNewTypeClass X] (x : X) : ‖x‖ = 0

Is this reasonable, or should I leave docs#norm_eq_zero alone and call the new lemma something like IndiscreteTopology.norm_eq_zero instead?

[Aaron Liu]

well we have isClopen_discrete and we have isClopen_iff, without going to mathlib, tell me what you think they say

[Eric Wieser]

Well, the first seems misnamed (arguably it should include _of_ or be namespaced), and the latter includes the _iff I'm proposing to add

[Jakub Nowak]

I think norm_eq_zero_iff is more appropriate name for docs#norm_eq_zero. docs#norm_eq_zero' similarly.
There's also docs#norm_ne_zero_iff which is just eq replaced with ne and it does have _iff.

[Kevin Buzzard]

Surely the very useful "|a|=0 iff a=0" is much much much more common than "in a rare edge case, |a|=0 always (because a was zero as zero is the only term of this type)" and thus deserves the smaller name? What about "norm_eq_zero_of_subsingleton"?

[Aaron Liu]

Kevin Buzzard said:

Surely the very useful "|a|=0 iff a=0" is much much much more common than "in a rare edge case, |a|=0 always (because a was zero as zero is the only term of this type)" and thus deserves the smaller name? What about "norm_eq_zero_of_subsingleton"?

funny, it's not subsingleton since the topology isn't Hausdorff.

[Kevin Buzzard]

Arguably the non-Hausdorff case is even more pathological!

[Aaron Liu]

you don't like it?

[Kevin Buzzard]

I'm just saying that in practice a working mathematician is 100 times more likely to see a normed vector space and use the theorem that |a|=0 iff a=0 than to see a vector space with a |.| function which satisfies the property that |a|=0 for all a, which is an argument for using the shorter name for the far more common application. I don't care either way about whether it's renamed or not, I'm just putting forward the argument for keeping things as they are. However keeping norm_eq_zero to mean the thing that everyone uses all the time means that it's hard to find a name for a theorem that says that in weird cases, the norm is always zero, so probably the renaming is best if there really is an actual use case for a theorem of the form "the norm of everything is zero" (and I can't think of one, but there might be one).

[Kevin Buzzard]

Consistency might be another argument for adding the iff, but my memory is that there are several other cases where there's no iff because it somehow "feels obvious" that the statement is an iff statement. Perhaps this conversation is an argument that iff should be added consistently in mathlib (maybe even in situations where there is no possible concievable usage for a theorem without the iff). But then of course you'll get people giving the same argument as mine above as to why the renaming should not happen.

[Jakub Nowak]

Eric Wieser said:

should I leave docs#norm_eq_zero alone and call the new lemma something like IndiscreteTopology.norm_eq_zero instead?

I understood is as that @Eric Wieser actually wants to add norm_eq_zero lemma?

[Eric Wieser]

yes, assuming a new [IndiscreteTopology X] typeclass

[Eric Wieser]

Which I guess is just generalizing docs#norm_of_subsingleton

[Kevin Buzzard]

Should docs#Finset.mem_singleton be renamed to mem_singleton_iff?

[Kevin Buzzard]

Note that docs#Set.mem_singleton says something totally different. This was the example that sprang to mind when I read this thread.

[Jakub Nowak]

There's docs#Finset.mem_singleton_self which is equivalent of docs#Set.mem_singleton.

[Jakub Nowak]

I would say, rename Finset.mem_singleton and Finset.notMem_singleton.

[Eric Wieser]

And docs#List.mem_singleton ?

[Aaron Liu]

The other option would be to rename Set.mem_singleton to Set.mem_singleton_self which matches the corresponding theorems for Finset Multiset List Array Vector

[Aaron Liu]

and then Set.mem_singleton_iff is renamed to Set.mem_singleton

[Jakub Nowak]

I would guess that docs#List.mem_singleton was first, and everything else followed.

[Aaron Liu]

this also matches with lemmas like docs#Option.mem_some_self and docs#Option.mem_some (with some instead of singleton)

[Jakub Nowak]

From my narrow point of view including _iff in names of theorems involving Iff is more common in mathlib. But looking at the theorems in Init.Data.List.Lemmas, it is not the case there.

[Aaron Liu]

interestingly, we also have docs#Option.mem_some_iff which is just a duplicate of Option.mem_some (this is in Init)