Proof of Urysohn's lemma. PR #900

Co-Authored-By: Cyril Cohen <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -36,6 +36,7 @@
 
 - in `mathcomp_extra.v`:
   + definition `min_fun`, notation `\min`
+  + new lemmas `maxr_absE`, `minr_absE`
 - in `classical_sets.v`:
   + lemmas `set_predC`, `preimage_true`, `preimage_false`
 - in `lebesgue_measure.v`:
@@ -63,22 +64,27 @@
 
 - in `classical_sets.v`:
   + lemma `Zorn_bigcup`
+  + lemmas `imsub1` and `imsub1P`
+
 - in file `boolp.v`,
   + lemmas `notP`, `notE`
   + new lemma `implyE`.
+  + new lemmas `contra_leP` and `contra_ltP`
+
 - in file `reals.v`:
   + lemmas `sup_sumE`, `inf_sumE`
 - in file `topology.v`:
   + lemma `ball_symE`
 - in file `normedtype.v`,
   + new definition `edist`.
-  + new lemmas `edist_ge0`, `edist_lt_ball`,
+  + new lemmas `edist_ge0`, `edist_neqNy`, `edist_lt_ball`,
     `edist_fin`, `edist_pinftyP`, `edist_finP`, `edist_fin_open`, 
     `edist_fin_closed`, `edist_pinfty_open`, `edist_sym`, `edist_triangle`, 
     `edist_continuous`, `edist_closeP`, and `edist_refl`.
 - in `constructive_ereal.v`:
   + lemmas `lte_pmulr`, `lte_pmull`, `lte_nmulr`, `lte_nmull`
   + lemmas `lte0n`, `lee0n`, `lte1n`, `lee1n`
+  + lemmas `fine0` and `fine1`
 - in `sequences.v`:
   + lemma `eseries_cond`
   + lemmas `eseries_mkcondl`, `eseries_mkcondr`
@@ -100,6 +106,21 @@
   + lemmas `Posz_snum_subproof` and `Negz_snum_subproof`
   + canonical instances `Posz_snum` and `Negz_snum`
 
+- in file `normedtype.v`,
+  + new definitions `edist_inf`, `uniform_separator`, and `Urysohn`.
+  + new lemmas `continuous_min`, `continuous_max`, `edist_closel`,
+    `edist_inf_ge0`, `edist_inf_neqNy`, `edist_inf_triangle`,
+    `edist_inf_continuous`, `edist_inf0`, `Urysohn_continuous`,
+    `Urysohn_range`, `Urysohn_sub0`, `Urysohn_sub1`, `Urysohn_eq0`,
+    `Urysohn_eq1`, `uniform_separatorW`, `normal_uniform_separator`,
+    `uniform_separatorP`, `normal_urysohnP`, and
+    `subset_closure_half`.
+
+- in file `topology.v`,
+  + new definition `normal_space`.
+  + new lemmas `filter_inv`, and `countable_uniform_bounded`.
+
+
 ### Changed
 
 - moved from `lebesgue_measure.v` to `real_interval.v`:
@@ -110,6 +131,7 @@
 
 - in `exp.v`:
   + lemmas `power_posD` (now `powRD`), `power_posB` (now `powRB`)
+- moved from `normedtype.v` to `topology.v`: `Rhausdorff`.
 
 - in `sequences.v`:
   + lemma `nneseriesrM` generalized and renamed to `nneseriesZl`

classical/boolp.v

@@ -497,6 +497,20 @@ Proof. by move=> Pxy; apply: contraNP => /Pxy/eqP. Qed.
 Lemma contra_eqP (T : eqType) (x y : T) (Q : Prop) : (~ Q -> x != y) -> x = y -> Q.
 Proof. by move=> Qxy /eqP; apply: contraTP. Qed.
 
+Lemma contra_leP {disp1 : unit} {T1 : porderType disp1} [P : Prop] [x y : T1] :
+  (~ P -> (x < y)%O) -> (y <= x)%O -> P.
+Proof.
+move=> Pxy yx; apply/asboolP.
+by apply: Order.POrderTheory.contra_leT yx => /asboolPn.
+Qed.
+
+Lemma contra_ltP {disp1 : unit} {T1 : porderType disp1} [P : Prop] [x y : T1] :
+  (~ P -> (x <= y)%O) -> (y < x)%O -> P.
+Proof.
+move=> Pxy yx; apply/asboolP.
+by apply: Order.POrderTheory.contra_ltT yx => /asboolPn.
+Qed.
+
 Lemma wlog_neg P : (~ P -> P) -> P.
 Proof. by move=> ?; case: (pselect P). Qed.
 

classical/classical_sets.v

@@ -1244,10 +1244,16 @@ Proof. by split=> fAY x; have := fAY x; rewrite !inE. Qed.
 Lemma image_subP {A Y f} : f @` A `<=` Y <-> {homo f : x / A x >-> Y x}.
 Proof. by split=> fAY x => [Ax|[y + <-]]; apply: fAY=> //; exists x. Qed.
 
-Lemma image_sub  {f : aT -> rT} {A : set aT} {B : set rT} :
+Lemma image_sub {f : aT -> rT} {A : set aT} {B : set rT} :
   (f @` A `<=` B) = (A `<=` f @^-1` B).
 Proof. by apply/propext; rewrite image_subP; split=> AB a /AB. Qed.
 
+Lemma imsub1 x A f : f @` A `<=` [set x] -> forall a, A a -> f a = x.
+Proof. by move=> + a Aa; apply; exists a. Qed.
+
+Lemma imsub1P x A f : f @` A `<=` [set x] <-> forall a, A a -> f a = x.
+Proof. by split=> [/(@imsub1 _)//|+ _ [a Aa <-]]; apply. Qed.
+
 Lemma image_setU f A B : f @` (A `|` B) = f @` A `|` f @` B.
 Proof.
 rewrite eqEsubset; split => b.

classical/mathcomp_extra.v

@@ -1392,3 +1392,27 @@ exists f; split => //.
 intro n; induction n; simpl; apply: proj2_sig.
 Qed.
 End dependent_choice_Type.
+
+Section max_min.
+Variable R : realFieldType.
+Import Num.Theory.
+
+Let nz2 : 2 != 0 :> R. Proof. by rewrite pnatr_eq0. Qed.
+
+Lemma maxr_absE (x y : R) : Num.max x y = (x + y + `|x - y|) / 2.
+Proof.
+apply: canRL (mulfK _) _ => //; rewrite ?pnatr_eq0//.
+case: lerP => _; (* TODO: ring *) rewrite [2]mulr2n mulrDr mulr1.
+  by rewrite addrACA subrr addr0.
+by rewrite addrCA addrAC subrr add0r.
+Qed.
+
+Lemma minr_absE (x y : R) : Num.min x y = (x + y - `|x - y|) / 2.
+Proof.
+apply: (addrI (Num.max x y)); rewrite addr_max_min maxr_absE. (* TODO: ring *)
+by rewrite -mulrDl addrACA subrr addr0 mulrDl -splitr.
+Qed.
+
+End max_min.
+
+Notation trivial := (ltac:(done)).

theories/constructive_ereal.v

@@ -327,6 +327,9 @@ split=> [|[->|[r r0 ->//]]]; last by rewrite real_leey/=.
 by case: x => [r r0 | _ |//]; [right; exists r|left].
 Qed.
 
+Lemma fine0 : fine 0 = 0%R :> R. Proof. by []. Qed.
+Lemma fine1 : fine 1 = 1%R :> R. Proof. by []. Qed.
+
 End ERealOrder_numDomainType.
 
 #[global] Hint Resolve lee01 lte01 : core.