Urysohn's Lemma

[zstone1]

Motivation for this change

A dramatic simplification of #871. The overall path of the proof is

1. First, normal has a simple filter-based equivalent definition
2. Given a closed set A, we can build a uniformity on T which measures "nearness to A", where each open set around A has a corresponding entourage. We use normality to define splitting entourages.
3. Given a closed set B which doesn't intersect A, we can separate them by normality. This dividing open set induces an entourage.
4. The gauge uniformity of this divider is a pseudometric, whose distance gives us the urysohn function.

The key ideas:

• One intuition for entourages is each gives a notion of "approximately" equal. So here, given open sets P and Q with A <= P <= closure P <= Q, we get an approximation of x ~ y <-> (Q x /\ Q y) \/ (~ closure P x /\ ~ closure P y). In other words, they are "both near A" or "both far from A" (or both). This gives us a basis for a filter, then we build this into a filter via smallest Filter
• The gauge is a pseudometric thanks to the countable_uniformity machinery. So instead of constructing a T -> R by hand, we construct a uniformity, and use the countability to guarantee a function. I have already used this countable_uniformity stuff 3 times this month. It has been an exceptionally convenient technique to avoid tinkering with arithmetic. That is, once for "countable products of pseudometrics", once for "uniform spaces are supremums of pseudometrics" and now for urysohn's lemma.
• The proof in Draft: Urysohn's Lemma via uniformities #871 manually built chains of A <= U1 <= closure U1 <= U2 <= closure U2 ... <= ~ B. But this proof is much nicer because it's phrased so a couple key applications of induction + filterI take care of it for us.
• This proof of urysohns is, as far as I can tell, original. It's not meaningfully easier, because it depends on the "countable_uniformity implies pseudometrizable" proof, which is really tough. But in a setting where that's already done, this proof is quite nice.
  • It avoids mentioning rational numbers entirely, and inducts over intersections of entourages. Much easier to work with!
  • Other than Hausdorff, it requires basically no topology of R.
  • No tricky details about countability and enumerations

Things done/to do

• [] added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Compatibility with MathComp 2.0

• I added the label TODO: HB port to make sure someone ports this PR to
  the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[zstone1]

Note, The stuff from #915 has now been rebased into this.

[affeldt-aist]

I wanted to read more seriously but ended up with only a minor linting commit. (You may want to use T3 instead of T``` and so on, it may help a little but surely the difficulty is not there ^_^.)

[zstone1]

Note, I've build some additional machinery to actually complete the proof without Hierarchy Builder. My approach is to show that pseudoMetrics admit an "extended" distance function into \bar R, and that the gauge pseudometric space is bounded, so the "extended" so fine \o edist is just the normal distance function. The notion of "bounded" should be included as a mixin in HB but for now this is fine.

[CohenCyril]

Fantastic. Maybe a small suggestion

Suggested change

	Lemma urysohn_seperation:
	exists (f : T -> R), [/\ continuous f,
	f @` A = [set 0], f @` B = [set 1] & range f `<=` `[0,1]].
	Lemma urysohn_separation:
	exists (f : T -> R), [/\ continuous f,
	f @` A = [set 0], f @` B = [set 1] & range f `<=` `[0,1]].

I'd actually export Ursyohn's lemma in the following form:

Definition Urysohn : set T -> set T -> T -> R := ...

In all of the cases make it so that Urysohn A B = Urysohn (closure A) (closure B)

We do a bunch of default cases for

• ~ normal_space T, A `&` B != set0 or A = set0 /\ B = set0 : Urysohn A B x = 2^-1
• A = set0: Urysohn A B x = 1
• B = set0: Urysohn A B x = 0

Then we have the following lemmas with fewer hypotheses:

Variables (A B : set T).

Lemma Urysohn_closurel : Urysohn (closure A) B = Urysohn A B.
Lemma Urysohn_closurer : Urysohn A (closure B) = Urysohn A B.

Let f := Urysohn A B.
Lemma range_Urysohn : range f `<=` `[0, 1].
Lemma Urysohn_continuous : continous f.

Lemma image_Urysohn_closurel : f @` closure A = f @` A.
Lemma image_Urysohn_closurer : f @` closure B = f @` B.

Variable (T_normal : normal_space T).
Lemma Urysohn_closure_sub0 : closure A `&` closure B = set0-> f @` A `<=` [set 0].
Lemma Urysohn_closure_sub1 : closure A `&` closure B = set0 -> f @` B `<=` [set 1].
Lemma Urysohn_closure_eq0 : A != set0 -> closure A `&` closure B = set0 -> f @` A = [set 0].
Lemma Urysohn_closure_eq1 : B != set0 -> closure A `&` closure B = set0 -> f @` B = [set 1].

Variables (A_closed : closed A) (B_closed : closed B).
Lemma Urysohn_sub0 : A `&` B = set0 -> f @` A `<=` [set 0].
Lemma Urysohn_sub1 : A `&` B = set0 -> f @` B `<=` [set 1].
Lemma Urysohn_eq0 : A != set0 -> A `&` B = set0 -> f @` A = [set 0].
Lemma Urysohn_eq1 : B != set0 -> A `&` B = set0 -> f @` B = [set 1].

[zstone1]

Yeah, this is pretty sensible. There's a couple math things worth mentioning here:

1. "Completely regular" (points and closed sets are separable by functions) <-> uniformizable
2. normal -> uniformizable (as witnessed by urysohn's lemma)
3. I only need normality to construct the underlying uniform spaces, and then pick the right gauge pseudometric. The function itself is doesn't really depend on normality of the space.
4. Uniform (but not necessarily normal) spaces have several excellent features, like a stone-cech compactification.

So, not only do I agree with the changes you describe here, but I actually want to generalize it to work uniform spaces in general. What I really need is triple of (A B : set X), (E : set (X *X )) with A * B & E = set0. Then what you have above becomes a specialization, where normality guarantees the existence of such an entourage.

[zstone1]

Well, I've finished what I mentioned above. I've learned three things:

1. The closed assumption is not necessary to build the function. It's only neccessary to ensure the existence of a separating entourage.
2. To make the separating function work out with no extra assumptions on the properties of E, I needed another minor lemma, that fun z => inf_(a in A) edist(z,a) is continuous. This is a not too hard, and I'm including it.
3. There's a thing here that would be "easier" with HB, but it's certainly not a requirement. Since normal => uniformizable, and I'd like to have Urysohn {X : uniformType} (A B : set X), it doesn't quite work on topological spaces. Not a blocker, but it will cause some mild duplication for now.

@CohenCyril updated. Let me know if this is close to your intention.

[CohenCyril]

This is close enough, but now there is an interface duplication. What do you think about doing the following change:

Definition Urysohn_sets A B := exists2 E, entourage E & A `*` B `&` E = set0.

Lemma Urysohn_setsS A A' B B' :
  A `<=` A' -> B `<=` B' -> Urysohn_sets A' B' -> Urysohn_sets A B.

Lemma normal_Urysohn : normal_space T ->
  forall A B, closed A -> closed B -> A `&` B = set0 -> Urysohn_sets A B.

Lemma normal_Urysohn_closure : normal_space T ->
  forall A B, closure A `&` closure B = set0 -> Urysohn_sets A B.

And then having a unique Urysohn function set T -> set T -> T -> R that does not satifsfy Urysohn (closure A) (closure B) = Urysohn A B. I think it's worth dropping this (little) bit of the interface to preserve the uniqueness of the Urysohn concept in the library, furthermore part of the interface can be recovered using normal_Urysohn_closure, so I do not think anything is really lost.

Now the theory looks as follows:

Implicit Types A B : set T.

Lemma Urysohn_continuous A B : continuous (Urysohn A B).

Lemma Urysohn_range A B : range (Urysohn A B) `<=` `[0,1].

Lemma Urysohn_sub0 A B : Urysohn_sets A B -> Urysohn A B @` A `<=` [set 0].

Lemma Urysohn_sub1 A B : Urysohn_sets A B -> Urysohn A B @` B `<=` [set 1].

Lemma Urysohn_eq0 A B : Urysohn_sets A B -> A !=set0 -> Urysohn A B @` A = [set 0].

Lemma Urysohn_eq0 A B : Urysohn_sets A B -> B !=set0 -> Urysohn A B @` B = [set 1].

[zstone1]

Ok, a more clear problem has arisen. One cannot apply Urysohn_range without a uniform space. But we'd like to define normal_Urysohn on a topological space. We have to explicitly declare the uniform space urysohn_uniformType A, but there seems to no nice way to automate this. In an even more serious case, we can't consolidate the continuity lemma. We need to prove @urysohn_uniformType T A implies continuity in T which requires an application of ury_gauge_nbhs.

This all seems to stem from something mathematical, not software related. Apparently what I said previously is a lie.

False: normal => uniformizable
True: normal + T1 => uniformizable

The moral of the story, as far as I can tell, is that even though the two constructions (urysohn functions on uniform spaces vs. normal spaces) are almost identical, there is apparently a meaningful distinction. I can imagine abstracting things with a "separable_by_functions (T : topologicalType)" mixin, but otherwise I can't figure out how to consolidate these.

[CohenCyril]

Out of curiosity is there a version of Urysohn's lemma such that f @^-1` [set 0] = A and f @^-1` [set 1] = B?
I'd expect so, but the wikipedia page does not mention it and your construction does not prove it (but does it?)

[zstone1]

Yes, this is T6, or perfectly normal. It's appreciably stronger than normal. There are a dozen or so equivalent definitions for T6, though. The Sogenfrey line (R with continuity from the left) is T6, but not metrizable.

Also for reference, we care about normal more than perfectly normal because

1. metrizable -> normal
2. compact -> normal
3. compact does not imply perfectly normal (thanks pi base for confirming: https://topology.pi-base.org/spaces?q=Compact%20%2B%20hausdorff%2B~%24T_6%24).

[CohenCyril]

@zstone1 I don't get it, you wrote that T1 + normal => uniformizable and that it isn't true without T1, but here you build a uniform space and I don't see the T1 hypothesis... What am I missing?

[zstone1]

The uniform space I built is substantially coarser than the original topology. (In particular, all of A collapses). Taking the sup over all A sup_uniformType (fun A => Uniform.class (urysohn_uniformType A)) works if your space is T1. But it's possible for this sup to still coarser than the original topology.

[CohenCyril]

Then we could embed a uniformity in the Uyrhson_sets predicate, couldn't we?

[zstone1]

We could. Is there a meaningful distinction between taking a UniformType as an argument, vs taking a TopologicalType and a Uniform.Class as arguments? We would also need Urysohn itself to take the uniform type.

But I think this is on the right track. If we really exploit classical logic, we take this one step further and put the uniformity into the definition
I think maybe this would work, but I need to make an attempt after work

Urysohn (T : topologicalType) (A B : set T) := if (pselect (exists UT : Uniform.class T, (@nbhs UT -> @nbhs T) /\ Urysohn_sets UT A B) then ... else (fun=> 0)

[zstone1]

Ok, this solves all our problems. There is now only one interface for Urysohn, and it depends on

Definition uniform_separator (A B : set T) :=
  exists (uT : @Uniform.class_of T^o) (E : set (T * T)), 
    let UT := Uniform.Pack uT in [/\ 
      @entourage UT E, A `*` B `&` E = set0 &
      (forall x, @nbhs UT UT x `<=` @nbhs T T x)].

Then we have uniform_separatorW and normal_uniform_separator which both construct uniform_separator in the cases of uniform or normal. Furthermore, the actual mechanics of urysohn_uniformType are never called upon, and hidden behind the existential in uniform_separator . This is not what I would write in a textbook but honestly it works pretty well.

[zstone1]

In fact, this interface is is equivalent to the desired property thanks to the weak topology of f. I just pushed a proof that

uniform_separatorP A B <-> exists (f : T -> R), [/\ continuous f,
  f @` A `<=` [set 0], f @` B `<=` [set 1] & range f `<=` `[0,1]].

That is reassuring, that the uniform_separator definition isn't missing anything important.

[CohenCyril]

That's great! Thanks for investigating this.

[CohenCyril]

Hence:

normal_space T <-> (forall A B, closed A -> closed B -> A `&` B = set0 -> uniform_separator A B)

?

[zstone1]

Yes, that's true. I agree it's a little cleaner to carry uniform_separator around instead of exists (f : T -> R), [/\ continuous f .... I've updated here. And in my next MR I will clean up the interface on the Tietze's theorem side as well.

[CohenCyril]

@zstone1 may I push a few cosmetic changes?

[zstone1]

@zstone1 may I push a few cosmetic changes?

Please do, I'm always happy to have the help.

[CohenCyril]

Please do, I'm always happy to have the help.

done

[zstone1]

Thanks. Anything else I should do before you can approve?

[CohenCyril]

No, that's all right

[zstone1]

Amazing. Thank you for the thorough review. The code is definitely better for it.