Zulip Chat Archive

Stream: maths

Topic: notations for uniform spaces


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Apr 15 2020 at 10:38):

How about making a ball function instead?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 15 2020 at 10:39):

including Gabriel.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 15 2020 at 10:41):

why is this a notation?

view this post on Zulip Mario Carneiro (Apr 15 2020 at 10:41):

instead of a function

view this post on Zulip Patrick Massot (Apr 15 2020 at 10:42):

Ok, give me a function name then.

view this post on Zulip Patrick Massot (Apr 15 2020 at 10:42):

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

view this post on Zulip Mario Carneiro (Apr 15 2020 at 10:42):

do we use the term entourage?

view this post on Zulip Patrick Massot (Apr 15 2020 at 10:42):

Sure

view this post on Zulip Mario Carneiro (Apr 15 2020 at 10:42):

uniform_space.ball?

view this post on Zulip Patrick Massot (Apr 15 2020 at 10:43):

At least in docstrings

view this post on Zulip Mario Carneiro (Apr 15 2020 at 10:43):

entourage.ball?

view this post on Zulip Patrick Massot (Apr 15 2020 at 10:43):

This will clash as soon as the metric namespace is open

view this post on Zulip Mario Carneiro (Apr 15 2020 at 10:43):

only if uniform_space is also open

view this post on Zulip Gabriel Ebner (Apr 15 2020 at 10:44):

uball?

view this post on Zulip Mario Carneiro (Apr 15 2020 at 10:44):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 15 2020 at 10:45):

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

view this post on Zulip Mario Carneiro (Apr 15 2020 at 10:45):

or use qualified names when you need to

view this post on Zulip Patrick Massot (Apr 15 2020 at 10:45):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 15 2020 at 10:46):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 15 2020 at 10:52):

I mean what's wrong with simple application?

view this post on Zulip Patrick Massot (Apr 15 2020 at 10:52):

I'll make a function anyway.

view this post on Zulip Patrick Massot (Apr 15 2020 at 10:52):

At least after reading some mathematical comments about all this.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 15 2020 at 10:54):

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

view this post on Zulip Patrick Massot (Apr 15 2020 at 10:54):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 15 2020 at 10:58):

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

view this post on Zulip Patrick Massot (Apr 15 2020 at 10:59):

Actually Bourbaki uses V(x)V(x).

view this post on Zulip 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]V[x]

view this post on Zulip Mario Carneiro (Apr 15 2020 at 11:02):

that wouldn't be confusing at all

view this post on Zulip Patrick Massot (Apr 15 2020 at 11:03):

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

view this post on Zulip Mario Carneiro (Apr 15 2020 at 11:04):

they work for long enough for the demo

view this post on Zulip Patrick Massot (Apr 15 2020 at 11:04):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 15 2020 at 11:05):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 15 2020 at 11:06):

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

view this post on Zulip Mario Carneiro (Apr 15 2020 at 11:07):

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

view this post on Zulip Mario Carneiro (Apr 15 2020 at 11:07):

more notations makes it harder to read, not easier

view this post on Zulip Patrick Massot (Apr 15 2020 at 11:08):

Which advanced filter notation?

view this post on Zulip Mario Carneiro (Apr 15 2020 at 11:08):

all this clever stuff with map and le on filters

view this post on Zulip Patrick Massot (Apr 15 2020 at 11:08):

This is not notation.

view this post on Zulip Mario Carneiro (Apr 15 2020 at 11:09):

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

view this post on Zulip Patrick Massot (Apr 15 2020 at 11:11):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 15 2020 at 11:16):

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

view this post on Zulip 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.

view this post on Zulip 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