Zulip Chat Archive

Stream: maths

Topic: topological space docs


view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:09):

Ok so after a ropey start (see my heq thread earlier) I made it through the topological_space.lean file today and wrote some docs on it: https://github.com/kbuzzard/mathlib/blob/docs-topspaces/docs/theories/topological_spaces.md . I needed to read this file for my work on schemes -- in particular I had to finally understand what a filter was and what they had to do with topological spaces.

view this post on Zulip Patrick Massot (Apr 14 2018 at 21:33):

You are a bit unfair with filters. You should at least explain that they allow to cover uniformly the cases of sequences and maps from topological spaces. And then slightly more exotic stuff like one-sided limits at some real. That's why Bourbaki invented them.

view this post on Zulip Patrick Massot (Apr 14 2018 at 21:35):

They also allow to mimic using sequential continuity and compactness for non-metric spaces

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:35):

One way to motivate them is to consider the ~16 variations on L'hopital's theorem that arise with lots of permutations of limits to different places in the domain and codomain

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:36):

I was just grumpy about them because they have actively stopped me doing what should be trivial stuff for a couple of days, because I didn't know what \Glb meant

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:37):

when I actually ploughed through the file and a lot of the imports, and set pp.all on occasionally etc etc and finally got to the bottom of things and discovered that F <= G iff G subseteq F

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:37):

then it all began to make sense

view this post on Zulip Patrick Massot (Apr 14 2018 at 21:37):

This is what this definition if compactness is about: a space is compact if every sequence has a converging subsequence,made true for all spaces

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:37):

The description of topological basis is also a bit grumpy; the point as I mentioned before is to say "a topological basis is a collection of sets satisfying these two axioms" and then fold in the connection to generating a topology

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:37):

I'm sure it's a very cute way to think about things

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:38):

yeah, I had to get up early this morning, I've been in a grumpy mood all day :-)

view this post on Zulip Patrick Massot (Apr 14 2018 at 21:38):

I'm defending filters here but zulip and gitter can testify I went through the same frustrations

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:39):

In fact I think the "filters are a complete lattice" angle should probably be emphasized more, since it underlies many of the filter-theoretic definitions

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:40):

A filter which is not bottom is called a proper filter fyi

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:40):

Mario, the reason I don't buy your explanation is that there is a standard definition of a basis of a topological space, which we all learn, and which is on Wikipedia, and which is not what is implemented, so all your protestations that it's a better way of doing it are cancelled out by the fact that every mathematician will be confused by the way it's done. I have flagged the relevant lemma which saves us.

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:41):

but it is that definition...

view this post on Zulip Patrick Massot (Apr 14 2018 at 21:41):

I think Mario had the right idea when I faced that:we keep filters but add lemmas translating to usual stuff in usual situations

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:41):

[explanation of why bases are done like that]

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:41):

Yes, I explictly flag the lemmas saying "oh look, compactness looks insane, here's the lemma you need"

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:41):

"bases look insane, here's the lemma you need"

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:41):

That's the philosophy of the docs

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:42):

https://en.wikipedia.org/wiki/Base_(topology)

A base is a collection B of subsets of X satisfying these two properties:
1. The base elements cover X.
2. Let B1, B2 be base elements and let I be their intersection. Then for each x in I, there is a base element B3 containing x and contained in I.

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:42):

Now I can use topological spaces in Lean, and this morning I couldn't.

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:42):

Right.

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:42):

Whereas you have generate_open

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:42):

it's the generate_open that makes it unusable

view this post on Zulip Patrick Massot (Apr 14 2018 at 21:42):

I'm sure you could also explain why filters are useful

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:42):

Any topological basis is a basis for the topology it generates

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:42):

the lemma you proved and I flagged makes the definition usable

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:43):

you can always satisfy that clause with refl

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:43):

My point is simply that if you want to prove that (a,b) x (c,d) is a basis of open sets for the standard topology on R^2, you cannot possibly do that from the definition

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:43):

but it's easy from the lemma

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:43):

Yes you can

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:43):

_you_ can

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:43):

a mathematician can't

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:44):

becuase they have no clue how to use generate_open

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:44):

Those are two different goals though

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:44):

you are trying to prove that some basis is a basis for something else, rather than just proving it's a basis

view this post on Zulip Patrick Massot (Apr 14 2018 at 21:44):

My wife says I must stop participating but please be nice :smiley:

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:45):

In maths, the proof goes "insert argument to prove that if x is in an open set U in R^2 then ther's some (a,b) x (c,d) in U containing x and now we're done

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:45):

in Lean the proof from the definition of basis goes "that, and then we have to prove something about generate_open"

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:45):

except now we don't because of the lemma

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:45):

You have a preconceived topology in that example

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:45):

yes, the one the mathematicans use :-)

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:45):

I'm talking about proving that some collection of sets is a basis full stop

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:46):

I know

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:46):

but that's a silly notion

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:46):

That's the one wikipedia discusses

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:46):

there's no generate_open there

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:46):

it's the generate_open which makes the definition a complete pain to work with

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:47):

and it's the lemma that saves us

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:47):

so I highlight the lemma

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:47):

that's all

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:47):

the lemmas are all there

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:47):

The generate_open is dischargable by refl, like I said

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:47):

I'm saying the definitions are silly, but that's OK because the lemmas are there

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:47):

yeah but I don't really know what that means

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:48):

and I know what the lemma means

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:48):

If S satisfies axioms 1 and 2, then it is a basis for (generate_open S)

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:48):

and a generic mathematician will come along

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:48):

with a proof of the two things in wikipedia

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:48):

and will want to prove that they have a basis

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:48):

and so they can use the lemma

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:49):

okay I get it you think the notion is useless

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:49):

right

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:49):

but I'm not saying it shouldn't be there

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:49):

I'm just explaining why I had to write the docs

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:49):

but the docs are

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:49):

and why they came out grumpy :-)

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:49):

that is an absurd definition of compact as well.

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:50):

It should be a theorem not a definition.

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:50):

But again it doesn't matter

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:51):

anyway, I am not grumpy any more :-)

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:51):

I'm not sure how much I want to defend this... I think Johannes thought the filter stuff would make everything neat and concise

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:51):

it doesn't matter

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:51):

I'm just taking a contrary position for a laugh really

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:51):

I'm really happy now

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:51):

I can work topological spaces

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:51):

I personally have a preference for standard point-set definitions

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:51):

and I'm hoping that other people with the same background as me (i.e. basically two courses in topology and that's it) can do the same

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:52):

but there are enough lemmas around to get rid of any filter claims you come across

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:52):

yeah, that's why Hausdorff is called t2 probably ;-)

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:52):

t2 is shorter :)

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:52):

I'm really happy with the lemmas. I was preparing a list of lemmas which you should have proved

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:52):

and it came out empty in the end

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:52):

Occasionally it would have size 1 or 2

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:53):

and then I'd find them :-)

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:53):

Props to @Johannes Hölzl too.

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:53):

yeah he gets the credit for most of this work

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:53):

It's a really nice complete library

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:53):

even though some definitions are theorems and some theorems are definitions ;-)

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:54):

I guess you guys can barely tell the difference

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:54):

you probably think I'm talking about unfolding or something

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:54):

it will teach you to forget about definitions and worry more about interfaces

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:54):

OK, enough CS baiting. Thank you for your library!

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:55):

I need to learn what this word interface means

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:55):

does API mean something to you?

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:57):

not really

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:57):

this is some way of talking to the theorems

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:57):

or something

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:58):

Are my docs some sort of attempt to make an API for mathematicians trying to use topological spaces in Lean?

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:58):

it's the idea that you encapsulate the underlying definition, somehow make it inaccessible, and then only use theorems that express properties of it

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:58):

encapsulate is another mystery

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:58):

these are all very CS words

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:59):

I understand that a mathematician will come along with a proof that every cover has a finite subcover and will want to deduce that their space is compact

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:59):

so I point them to the lemma which says this

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:59):

[and make some snarky remark probably about how the definition is something else]

view this post on Zulip Mario Carneiro (Apr 14 2018 at 21:59):

Category theory does this a lot, for example: A product of two objects is some object with a universal property, so that you can only use the universal property to prove stuff rather than unfolding whatever the product is "actually" defined to be in a particular category

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 21:59):

universal properties I understand

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:00):

but I don't understand why this is an argument for giving an unrecognisable definition of compact

view this post on Zulip Mario Carneiro (Apr 14 2018 at 22:00):

A biconditional is also a "universal property", in a sense

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:00):

biconditional is a theorem of the form X iff Y?

view this post on Zulip Mario Carneiro (Apr 14 2018 at 22:00):

it tells you everything you ever need to know about the definition, without actually telling you what the definition is

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:00):

I see

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:00):

but you really need to know where the theorem is

view this post on Zulip Mario Carneiro (Apr 14 2018 at 22:01):

yes, that's the public part

view this post on Zulip Mario Carneiro (Apr 14 2018 at 22:01):

the definition is the private part

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:01):

Maybe I saw this in java once

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:01):

your variables are private

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:01):

and you make some functions which lets the user change them

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:01):

or read them

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:01):

without actually letting them fiddle with them directly

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:01):

sorry, methods

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:02):

but I didn't realise this had anything to do with topological spaces at the time

view this post on Zulip Mario Carneiro (Apr 14 2018 at 22:02):

One reasonably basic example of a gnarly construction is the Kuratowski pair (a,b) = {{a}, {a, b}}

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:02):

eew

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:02):

eew

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:02):

I see

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:03):

that's a great example

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:03):

we just need (a,b) = (c,d) iff a=c and b=d

view this post on Zulip Mario Carneiro (Apr 14 2018 at 22:03):

exactly

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:03):

so we point the user to where that is proved

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:03):

and they can't see the disgusting truth behind it all

view this post on Zulip Mario Carneiro (Apr 14 2018 at 22:04):

and later, we might want to change the definition for some reason to, say, {{0,a}, {1, b}} and that's okay as long as we can still prove the defining property, since no user depended on the specific construction

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:04):

but the compactness thing is different. We go for Kuratowski because all the choices are horrible and this one is the least horrible

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:04):

I see

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:04):

it's not completely different

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:05):

you are reserving the right to invent some even more weird thing that is better than filters

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:05):

and then change the definition of compactness

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:05):

because it compiles better on a quantum computer or whatever

view this post on Zulip Mario Carneiro (Apr 14 2018 at 22:06):

or even just the point-set definition

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:06):

I see. In fact you could just play that trump card and that would shut me up

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:06):

you should just say "Kevin, you don't understand, the definition we have here works better if your machine has 8 cores"

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:06):

and I would have no response

view this post on Zulip Mario Carneiro (Apr 14 2018 at 22:06):

the real point is that it shouldn't matter what the actual definition is, and if it does you're doing it wrong

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:06):

This is different to mathematics

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:07):

If you wrote a maths book with some weird definitions of things

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:07):

and then proved theorems which said that they were the same as everyone else's definition

view this post on Zulip Mario Carneiro (Apr 14 2018 at 22:07):

there's also the pedagogical angle, but that's a different issue

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:07):

people would be confused as to why you were doing it

view this post on Zulip Mario Carneiro (Apr 14 2018 at 22:07):

I don't think that exact thing is unheard of though

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:07):

and you can't answer "this definition works better if you have 8 brains"

view this post on Zulip Mario Carneiro (Apr 14 2018 at 22:08):

your new definition might be suitable to a particular sort of generalization, for example

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:08):

As you are probably aware, I am extremely interested in the pedagogical angle

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:08):

and have very little understanding of stuff like run time analysis and other CS-related matters

view this post on Zulip Mario Carneiro (Apr 14 2018 at 22:09):

in the pedagogical view, you might redefine the same thing several times depending on the current teaching goals

view this post on Zulip Mario Carneiro (Apr 14 2018 at 22:09):

the new definition may not even be the same as earlier ones, although it is usually a generalization or provably equivalent

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:10):

So ultimately I should not care about your definitions, my main aim is to make sure that the interfaces are there.

view this post on Zulip Mario Carneiro (Apr 14 2018 at 22:10):

exactly

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:10):

OK maybe tomorrow I will degrump it a bit :-)

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:11):

but now I have to make a birthday present

view this post on Zulip Mario Carneiro (Apr 14 2018 at 22:11):

lol it's my birthday so I'll just pretend that's for me ;)

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:11):

ha ha it's for my son's GF

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:11):

happy birthday

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 22:12):

I'm not entirely sure you'd want a plastic T anyway

view this post on Zulip Mario Carneiro (Apr 14 2018 at 22:13):

good mathlib docs are a good present :)

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:32):

OK well seeing as it's your birthday I de-grumped the docs a bit.

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:32):

even though it's strictly speaking not even your birthday any more where I'm sitting

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:33):

I'm now about to get onto the job I meant to do today, which was to prove that Spec(R) is compact using some argument involving bases :-)

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:33):

now I understand the interface better :-)

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:33):

Thanks as ever, by the way.

view this post on Zulip Mario Carneiro (Apr 14 2018 at 23:35):

I forget if the contrapositive form of the compactness definition is there: a collection of closed sets with the finite intersection property has nonempty intersection

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:35):

I didn't see it

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:36):

and I almost mentioned it as a theorem which should be there

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:36):

but then I decided I'd never used it in my life :-)

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:36):

I almost mentioned it the other day when Simon was asking whether the same was true for an arbitrary set

view this post on Zulip Mario Carneiro (Apr 14 2018 at 23:37):

I guess it is somewhat similar to the filter definition

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:40):

Hmm, I've just realised that I want that a mathlib-basis is a Wikipedia-basis

view this post on Zulip Mario Carneiro (Apr 14 2018 at 23:40):

that's just the first two parts of the definition

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:42):

oh sorry I don't mean that

view this post on Zulip Mario Carneiro (Apr 14 2018 at 23:43):

If h1 and h2 are proofs of the two axioms, then <h1, h2, rfl> is a proof it's a mathlib-basis

view this post on Zulip Mario Carneiro (Apr 14 2018 at 23:43):

that's what I've been saying

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:43):

is_topological_basis_of_open_of_nhds

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:44):

I mean the converse of that

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:44):

Yes, sorry, I understand now

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:44):

I was talking nonsense at some points earlier

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:44):

when I said "wikipedia definition"

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:44):

I sometimes meant "hypotheses in is_topological_basis_of_open_of_nhds"

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:44):

:-/

view this post on Zulip Mario Carneiro (Apr 14 2018 at 23:45):

mem_nhds_of_is_topological_basis is the easiest way to get converses of that stuff

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:46):

https://topospaces.subwiki.org/wiki/Basis_for_a_topological_space

view this post on Zulip Mario Carneiro (Apr 14 2018 at 23:46):

but there should be a theorem saying that a basis element is open

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:46):

there's a website (which I've never heard of) giving that as the definition.

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:47):

This is evidence that I am very fluid with what my definition is :-/

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:47):

mem_nhds means I might have to get my hands dirty with neighbourhoods maybe :-/

view this post on Zulip Mario Carneiro (Apr 14 2018 at 23:47):

which statement are you going for specifically?

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:49):

if B is a basis then I want that for all U open and for all x in U, there's V in B with x in V in U

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:49):

because as we all know

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:50):

50% of the time I will swear blind that this is the definition of a basis in Wikipedia

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:50):

and I don't want to do induction on generate_open

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:50):

I want this to be there on a plate

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:50):

Kenny proved it

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:51):

in a file called temp.lean :-)

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:51):

but I was trying to avoid importing this file

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:51):

because its name looked a bit ominous

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:52):

I can do this myself

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:52):

The lemmas I need are all there

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:52):

I just need to glue them

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:52):

This morning I didn't know what nhds a was

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:52):

I have to remember that I'm not scared of it any more

view this post on Zulip Mario Carneiro (Apr 14 2018 at 23:54):

I can add these to the file:

lemma is_open_of_is_topological_basis {s : set α} {b : set (set α)}
  (hb : is_topological_basis b) (hs : s ∈ b) : _root_.is_open s :=
is_open_iff_mem_nhds.2 $ λ a as,
(mem_nhds_of_is_topological_basis hb).2 ⟨s, hs, as, subset.refl _⟩

lemma mem_subset_basis_of_mem_open {b : set (set α)}
  (hb : is_topological_basis b) {a:α} (u : set α) (au : a ∈ u)
  (ou : _root_.is_open u) : ∃v ∈ b, a ∈ v ∧ v ⊆ u :=
(mem_nhds_of_is_topological_basis hb).1 $ mem_nhds_sets ou au

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:55):

It's the easy way of is_open_iff_mem_nhds I need and then I'm done :-)

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:56):

yeah, what you said

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:56):

I'd vote for them definitely.

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:56):

Then I can eschew temp.lean completely

view this post on Zulip Mario Carneiro (Apr 14 2018 at 23:56):

I like mem_nhds_of_is_topological_basis because it generalizes well to all sorts of bounded quantification over open sets that comes up in topology, like continuity or compactness that can be stated with basis sets

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:57):

I didn't like it until today because of the obscure definition of nhds

view this post on Zulip Kevin Buzzard (Apr 14 2018 at 23:59):

but again there was a lemma -- in this case mem_nhds_sets_iff -- which made this clear

view this post on Zulip Kevin Buzzard (Apr 15 2018 at 00:01):

or even nhds_sets, which I mention in the docs

view this post on Zulip Kevin Buzzard (Apr 15 2018 at 00:02):

I see. I'm mentioning all the results that a mathematician needs for the interface.

view this post on Zulip Kevin Buzzard (Apr 15 2018 at 00:17):

eew, exists v \in B -- I have to run classical.some twice to get that v is in B

view this post on Zulip Mario Carneiro (Apr 15 2018 at 00:18):

You can use exists.fst for the v \in B hypothesis

view this post on Zulip Kevin Buzzard (Apr 15 2018 at 00:18):

That means exists v in B, P (B a set) unravels to exists v in X, exists H : v in B, ...

view this post on Zulip Kevin Buzzard (Apr 15 2018 at 00:19):

Why not unravel to exists v in X, v in B and ...

view this post on Zulip Mario Carneiro (Apr 15 2018 at 00:19):

You can also use exists v : B, P to pack them both into one

view this post on Zulip Kevin Buzzard (Apr 15 2018 at 00:19):

yeah but you wrote v in B not me ;-)

view this post on Zulip Mario Carneiro (Apr 15 2018 at 00:19):

because that same translation works for a wide variety of binders

view this post on Zulip Kevin Buzzard (Apr 15 2018 at 00:20):

I don't know what a binder is

view this post on Zulip Mario Carneiro (Apr 15 2018 at 00:20):

A thing that introduces a bound variable

view this post on Zulip Mario Carneiro (Apr 15 2018 at 00:20):

like exists or forall or lambda

view this post on Zulip Kevin Buzzard (Apr 15 2018 at 00:20):

somehow I thought that there were only about three of these

view this post on Zulip Mario Carneiro (Apr 15 2018 at 00:20):

or Glb or Lub

view this post on Zulip Kevin Buzzard (Apr 15 2018 at 00:21):

but you're saying "exists v \in B" is somehow another one

view this post on Zulip Mario Carneiro (Apr 15 2018 at 00:21):

or indexed intersection

view this post on Zulip Kevin Buzzard (Apr 15 2018 at 00:22):

I see.

view this post on Zulip Mario Carneiro (Apr 15 2018 at 00:22):

No, I'm saying that every binder has the translation Q a R b, p a => Q a, Q (_ : a R b), p a where Q is any binder

view this post on Zulip Mario Carneiro (Apr 15 2018 at 00:22):

and R is any infix operator

view this post on Zulip Kevin Buzzard (Apr 15 2018 at 00:22):

unknown identifier 'exists.fst'

view this post on Zulip Mario Carneiro (Apr 15 2018 at 00:23):

should be in logic.basic

view this post on Zulip Mario Carneiro (Apr 15 2018 at 00:23):

It's Exists.fst so you can use projections

view this post on Zulip Kevin Buzzard (Apr 15 2018 at 00:24):

capital E, got it

view this post on Zulip Kevin Buzzard (Apr 15 2018 at 00:25):

you use Q again

view this post on Zulip Patrick Massot (Apr 15 2018 at 09:51):

OK well seeing as it's your birthday I de-grumped the docs a bit.

I think it still misses the main point of using filters: you have limits at a point and limits when a real variable or a natural number goes to infinity gathered in a single definition. For instance uniqueness of limit that you mention in your doc is proved for all three (and more) situations at once. This has nothing to do with "non-mathematical points such as running times".

view this post on Zulip Kevin Buzzard (Apr 15 2018 at 10:31):

I just don't know anything about how filters are used in practice so am in no position to be able to write those parts of the docs properly. I've never had to use them before and I don't really care about explaining them for this reason; I just wanted to get down the things I needed to know myself.

view this post on Zulip Johannes Hölzl (Apr 15 2018 at 17:00):

@Kevin Buzzard just added your documentation, I guess we can add more comments on filters later.
I think one problem why there is not a lot of knowledge about filters (or nets) in math, is that it is obvious and usually something you don't need to think about. But we are in a formal system, so we are either forced to generalize over limits (using filters or nets) or we produce a lot of duplication (as Mario and Patrick mentioned). We can avoid them and define things like compact using open covers etc. But some proofs get much more concise using the fact that you can use the complete lattice (and even category theory) properties properties of filters. Currently it is not always intuitive to work with filters, but maybe with more automation and better syntax notations and support from the parser it may get better.
In the end they are a powerful abstraction, and as most abstractions it takes some time to learn it.

view this post on Zulip Kevin Buzzard (Apr 15 2018 at 17:24):

Yeah, Mario convinced me not to worry about what was a definition and what was a theorem, as long as the theorems were all there.

view this post on Zulip Sebastien Gouezel (Apr 15 2018 at 19:38):

There is a very expressive way to use filters, with the word eventually.
def eventually {α : Type} (P : α → Prop) (f : filter α) := {x | P x} ∈ f.sets
Then if you want to say that, eventually, some function u defined on nat is nonnegative, you write
eventually (λn, 0 ≤ u n) at_top
If you want to say the same thing around a point x, say (which corresponds to a filter at x), you just write it as
eventually (λy, 0 ≤ f y) (at x)
In this way, you can also write readable definitions of limits, or essentially whatever involves filters. This is the only way I use filters in Isabelle, and I was essentially never stuck.

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

@Johannes Hölzl what do you think about adding (and using) this definition?

view this post on Zulip Johannes Hölzl (Apr 16 2018 at 06:37):

I'm fine with adding this definition, especially with a corresponding quantifier notation (and also its dual the frequently quantifier). I'm just not sure if we should abandon the f.sets notation or keep both.

view this post on Zulip Mario Carneiro (Apr 16 2018 at 06:41):

I want to refactor the filter stuff so that .sets is superfluous, i.e. s \in f means s \in f.sets. I guess we can support eventually if it's a reducible definition, but I don't like the idea of duplicating everything for this purpose

view this post on Zulip Johannes Hölzl (Apr 16 2018 at 07:04):

Setting up a has_mem for filter is surely a good idea.


Last updated: May 11 2021 at 16:22 UTC