notations for uniform spaces

Stream: maths

[Patrick Massot]

@Sebastien Gouezel and @Yury G. Kudryashov. In relation to my work on sequential compactness and our filter.basic efforts, how would you like to see things like:

import topology.uniform_space.basic

variable {α : Type*}

open_locale uniformity

localized "notation `ball_[` V `] ` x:55 := (prod.mk x) ⁻¹' V" in uniformity

localized "infix `○`:55 := comp_rel" in uniformity

lemma mem_ball_comp {V W : set (α × α)} {x y z} (h : y ∈ ball_[V] x) (h' : z ∈ ball_[W] y) :
  z ∈ ball_[V ○ W] x :=
prod_mk_mem_comp_rel h h'

lemma is_open_iff_ball_subset [uniform_space α] {s : set α} :
  is_open s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball_[V] x ⊆ s :=
begin
  simp_rw [is_open_iff_mem_nhds, nhds_eq_comap_uniformity],
  exact iff.rfl,
end

[Patrick Massot]

The circle thing is only bringing in Bourbaki's notation. The main goal here is the ball notation, trying to make it easier for our casual readers to bridge the gap from metric spaces to uniform spaces.

[Gabriel Ebner]

How about making a ball function instead?

[Patrick Massot]

I'm pinging Sébastien and Yury because I hope they have an opinion, but of course everybody is welcome to answer.

[Patrick Massot]

including Gabriel.

[Patrick Massot]

I don't want a name clash with metric space balls. Although this notation suggests they are the same, type theory doesn't quite agree.

[Patrick Massot]

Actually even on paper ball_[V] is more general in metric spaces, because not every entourage belongs to the obvious basis.

[Mario Carneiro]

why is this a notation?

[Mario Carneiro]

instead of a function

[Patrick Massot]

Ok, give me a function name then.

[Patrick Massot]

(ball is not good enough, as I told Gabriel)

[Mario Carneiro]

do we use the term entourage?

[Patrick Massot]

Sure

[Mario Carneiro]

uniform_space.ball?

[Patrick Massot]

At least in docstrings

[Mario Carneiro]

entourage.ball?

[Patrick Massot]

This will clash as soon as the metric namespace is open

[Mario Carneiro]

only if uniform_space is also open

[Gabriel Ebner]

uball?

[Mario Carneiro]

I feel like this kind of argument defeats the purpose of namespaces

[Mario Carneiro]

yes, things will clash if you open too many namespaces at once. Maybe don't do that then

[Patrick Massot]

It defeats it only when considering two namespaces that are likely to be open together.

[Mario Carneiro]

or use qualified names when you need to

[Patrick Massot]

In this case I guess this will be common only in very foundational files.

[Mario Carneiro]

I should think this will only be in files about uniform spaces, that aren't also doing metric space stuff

[Mario Carneiro]

there might be one theorem about the relation between ball and uball and that's it

[Mario Carneiro]

and I would definitely expect the use of qualified names in that theorem for clarity if nothing else

[Mario Carneiro]

also, the notation doesn't appear to be doing that much work for you. It doesn't seem any more readable than ball V x

[Patrick Massot]

Oh sure, the brackets are here only because the parser doesn't like two variables in a row.

[Mario Carneiro]

I mean what's wrong with simple application?

[Patrick Massot]

I'll make a function anyway.

[Patrick Massot]

At least after reading some mathematical comments about all this.

[Mario Carneiro]

Does this relate to a mathematical construction in the books? I mean I get why you call this a ball but is the notation ball_V x common?

[Mario Carneiro]

TBH I don't know many books that cover uniform spaces in the first place

[Patrick Massot]

Not that I know, otherwise I wouldn't ask for comments.

[Patrick Massot]

I only read Bourbaki on this topic, and they don't really care about readers who understand slowly.

[Mario Carneiro]

I usually use wikipedia as a source for formal math. It's pretty rare that I need to go beyond wikipedia level coverage on a library topic

[Patrick Massot]

https://en.wikipedia.org/wiki/Uniform_space#Entourage_definition has the notation $V[x]$.

[Patrick Massot]

Actually Bourbaki uses $V(x)$.

[Mario Carneiro]

I suppose, if you defined entourage A := set (A x A) you could have a coe_to_fun so that V x means $V[x]$

[Mario Carneiro]

that wouldn't be confusing at all

[Patrick Massot]

Mario, you know coercions to functions don't work in Lean 3...

[Mario Carneiro]

they work for long enough for the demo

[Patrick Massot]

That's true, but we are discussing things to include in mathlib here.

[Mario Carneiro]

For mathlib, I wouldn't even bother with notations or functions for any of this, but maybe that's just me

[Mario Carneiro]

I mean uniform spaces have already muddled through all of this without the definition

[Mario Carneiro]

if we're talking about only what's needed to make the mathematical arguments work, this is all window dressing, prod.mk x \-1' V works fine

[Patrick Massot]

But this uniform_space.basic is really hard to read, for no good reason at all.

[Mario Carneiro]

I think that advanced filter notation is what makes it the hardest to read

[Mario Carneiro]

more notations makes it harder to read, not easier

[Patrick Massot]

Which advanced filter notation?

[Mario Carneiro]

all this clever stuff with map and le on filters

[Patrick Massot]

This is not notation.

[Mario Carneiro]

it's a definition for a more basic set level expression

[Patrick Massot]

Yeah! We reached the Mario point! He didn't need all that in metamath :wink:

[Mario Carneiro]

It's all very "clever" in the bad sense of the word. Everyone struggles with it at first, and I'm not sure what has been gained; not proof length, not compilation speed, it is less characters in statements but that's a dubious gain if it means more definitions

[Mario Carneiro]

I would much prefer that uniform spaces look like the wikipedia definition

[Patrick Massot]

I think Johannes went a bit too far in this direction in this file, but the overall idea is good.

[Mario Carneiro]

I think the idea should be leveraged for shorter proofs where applicable, but shouldn't be in the definitions