## Stream: maths

### Topic: notations for uniform spaces

#### Patrick Massot (Apr 15 2020 at 10:36):

@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 (Apr 15 2020 at 10:37):

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.

#### Patrick Massot (Apr 15 2020 at 10:39):

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

#### Patrick Massot (Apr 15 2020 at 10:39):

including Gabriel.

#### Patrick Massot (Apr 15 2020 at 10:40):

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 (Apr 15 2020 at 10:40):

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

#### Mario Carneiro (Apr 15 2020 at 10:41):

why is this a notation?

#### Patrick Massot (Apr 15 2020 at 10:42):

Ok, give me a function name then.

#### Patrick Massot (Apr 15 2020 at 10:42):

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

#### Mario Carneiro (Apr 15 2020 at 10:42):

do we use the term entourage?

Sure

#### Mario Carneiro (Apr 15 2020 at 10:42):

uniform_space.ball?

#### Patrick Massot (Apr 15 2020 at 10:43):

At least in docstrings

#### Mario Carneiro (Apr 15 2020 at 10:43):

entourage.ball?

#### Patrick Massot (Apr 15 2020 at 10:43):

This will clash as soon as the metric namespace is open

#### Mario Carneiro (Apr 15 2020 at 10:43):

only if uniform_space is also open

#### Gabriel Ebner (Apr 15 2020 at 10:44):

uball?

#### Mario Carneiro (Apr 15 2020 at 10:44):

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

#### Mario Carneiro (Apr 15 2020 at 10:45):

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

#### Patrick Massot (Apr 15 2020 at 10:45):

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

#### Mario Carneiro (Apr 15 2020 at 10:45):

or use qualified names when you need to

#### Patrick Massot (Apr 15 2020 at 10:45):

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

#### Mario Carneiro (Apr 15 2020 at 10:46):

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

#### Mario Carneiro (Apr 15 2020 at 10:46):

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

#### Mario Carneiro (Apr 15 2020 at 10:47):

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

#### Mario Carneiro (Apr 15 2020 at 10:49):

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 (Apr 15 2020 at 10:51):

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

#### Mario Carneiro (Apr 15 2020 at 10:52):

I mean what's wrong with simple application?

#### Patrick Massot (Apr 15 2020 at 10:52):

I'll make a function anyway.

#### Mario Carneiro (Apr 15 2020 at 10:53):

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 (Apr 15 2020 at 10:54):

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

#### Patrick Massot (Apr 15 2020 at 10:55):

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

#### Mario Carneiro (Apr 15 2020 at 10:57):

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 (Apr 15 2020 at 10:58):

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

#### Patrick Massot (Apr 15 2020 at 10:59):

Actually Bourbaki uses $V(x)$.

#### Mario Carneiro (Apr 15 2020 at 11:01):

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 (Apr 15 2020 at 11:02):

that wouldn't be confusing at all

#### Patrick Massot (Apr 15 2020 at 11:03):

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

#### Mario Carneiro (Apr 15 2020 at 11:04):

they work for long enough for the demo

#### Patrick Massot (Apr 15 2020 at 11:04):

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

#### Mario Carneiro (Apr 15 2020 at 11:04):

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

#### Mario Carneiro (Apr 15 2020 at 11:05):

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

#### Mario Carneiro (Apr 15 2020 at 11:06):

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 (Apr 15 2020 at 11:06):

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

#### Mario Carneiro (Apr 15 2020 at 11:07):

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

#### Mario Carneiro (Apr 15 2020 at 11:07):

more notations makes it harder to read, not easier

#### Mario Carneiro (Apr 15 2020 at 11:08):

all this clever stuff with map and le on filters

#### Patrick Massot (Apr 15 2020 at 11:08):

This is not notation.

#### Mario Carneiro (Apr 15 2020 at 11:09):

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

#### Patrick Massot (Apr 15 2020 at 11:11):

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

#### Mario Carneiro (Apr 15 2020 at 11:15):

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 (Apr 15 2020 at 11:16):

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

#### Patrick Massot (Apr 15 2020 at 11:22):

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

#### Mario Carneiro (Apr 15 2020 at 11:25):

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

Last updated: May 09 2021 at 11:09 UTC