Product embedding (#768)

* swapping machines

* proof of open map

* hausdorff accessible

* weak products equivalent

* changelog

* strengthen join_product_weak

* cleaning up proofs

* typos

* adding local notations for proof legibility

* merging product stuff

* fixing changelog

* specialized conjunctions to use less brackets and splits

* fixing grammar

* fix changelog

* fixing build

* more build fixes

---------

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>

Author: 2 people

CHANGELOG_UNRELEASED.md

@@ -69,6 +69,17 @@
   + new lemmas `pi_continuous`, `quotient_continuous`, and
     `repr_comp_continuous`.
 
+- in file `boolp.v`,
+  + new lemma `forallp_asboolPn2`.
+- in file `classical_sets.v`,
+  + new lemma `preimage_range`.
+- in file `topology.v`,
+  + new definitions `hausdorff_accessible`, `separate_points_from_closed`, and 
+    `join_product`.
+  + new lemmas `weak_sep_cvg`, `weak_sep_nbhsE`, `weak_sep_openE`, 
+    `join_product_continuous`, `join_product_open`, `join_product_inj`, and 
+    `join_product_weak`. 
+
 ### Changed
 
 - in `fsbigop.v`:

classical/boolp.v

@@ -674,6 +674,14 @@ split=> [[x Px NQx] /(_ x Px)//|]; apply: contra_notP => + x Px.
 by apply: contra_notP => NQx; exists x.
 Qed.
 
+Lemma forallp_asboolPn2 {T} {P Q : T -> Prop} :
+  reflect (forall x : T, ~ P x \/ ~ Q x) (~~ `[<exists2 x : T, P x & Q x>]).
+Proof.
+apply: (iffP idP)=> [/asboolPn NP x|NP].
+  by move/forallPNP : NP => /(_ x)/and_rec/not_andP.
+by apply/asboolP=> -[x Px Qx]; have /not_andP := NP x; exact.
+Qed.
+
 Module FunOrder.
 Section FunOrder.
 Import Order.TTheory.

classical/classical_sets.v

@@ -1278,6 +1278,9 @@ Proof. by case=> [t ?]; exists (f t). Qed.
 Lemma preimage_image f A : A `<=` f @^-1` (f @` A).
 Proof. by move=> a Aa; exists a. Qed.
 
+Lemma preimage_range {A B : Type} (f : A -> B) : f @^-1` (range f) = [set: A].
+Proof. by rewrite eqEsubset; split=> x // _; exists x. Qed.
+
 Lemma image_preimage_subset f Y : f @` (f @^-1` Y) `<=` Y.
 Proof. by move=> _ [t /= Yft <-]. Qed.
 

theories/normedtype.v

@@ -3022,26 +3022,26 @@ Qed.
 Lemma nbhs_open_ereal_lt r (f : R -> R) : r < f r ->
   nbhs r%:E [set y | y < (f r)%:E]%E.
 Proof.
-move=> xfx; rewrite nbhsE /=; eexists; split; last by move=> y; exact.
+move=> xfx; rewrite nbhsE /=; eexists; last by move=> y; exact.
 by split; [apply open_ereal_lt_ereal | rewrite /= lte_fin].
 Qed.
 
 Lemma nbhs_open_ereal_gt r (f : R -> R) : f r < r ->
   nbhs r%:E [set y | (f r)%:E < y]%E.
 Proof.
-move=> xfx; rewrite nbhsE /=; eexists; split; last by move=> y; exact.
+move=> xfx; rewrite nbhsE /=; eexists; last by move=> y; exact.
 by split; [apply open_ereal_gt_ereal | rewrite /= lte_fin].
 Qed.
 
 Lemma nbhs_open_ereal_pinfty r : (nbhs +oo [set y | r%:E < y])%E.
 Proof.
-rewrite nbhsE /=; eexists; split; last by move=> y; exact.
+rewrite nbhsE /=; eexists; last by move=> y; exact.
 by split; [apply open_ereal_gt_ereal | rewrite /= ltry].
 Qed.
 
 Lemma nbhs_open_ereal_ninfty r : (nbhs -oo [set y | y < r%:E])%E.
 Proof.
-rewrite nbhsE /=; eexists; split; last by move=> y; exact.
+rewrite nbhsE /=; eexists; last by move=> y; exact.
 by split; [apply open_ereal_lt_ereal | rewrite /= ltNyr].
 Qed.
 
@@ -3372,7 +3372,7 @@ move=> oU; have [->|U0] := eqVneq U set0.
 apply/seteqP; split=> [x Ux|x [p _ Ipx]]; last exact: bigcup_ointsub_sub Ipx.
 suff [q Iqx] : exists q, bigcup_ointsub U q x.
   by exists q => //=; rewrite in_setE; case: Iqx => A [[_ _ +] ? _]; exact.
-have : nbhs x U by rewrite nbhsE /=; exists U; split => //.
+have : nbhs x U by rewrite nbhsE /=; exists U.
 rewrite -nbhs_ballE /nbhs_ball /nbhs_ball_ => -[_/posnumP[r] xrU].
 have /rat_in_itvoo[q qxxr] : (x - r%:num < x + r%:num)%R.
   by rewrite ltr_subl_addr -addrA ltr_addl.
@@ -3886,7 +3886,7 @@ move=> C D FC f_D; have {}f_D :
   have exPj : forall j, exists Bj, open_nbhs (f j) Bj /\ Bj `<=` E ord0 j.
     move=> j; have := f_E ord0 j; rewrite nbhsE => - [Bj].
     by rewrite row_simpl'; exists Bj.
-  exists [set g | forall j, (get (Pj j)) (g j)]; split; last first.
+  exists [set g | forall j, (get (Pj j)) (g j)]; last first.
     move=> g Pg; apply: sED => i j; rewrite ord1 row_simpl'.
     by have /getPex [_ /(_ _ (Pg j))] := exPj j.
   split; last by move=> j; have /getPex [[]] := exPj j.

theories/sequences.v

@@ -1294,8 +1294,7 @@ Lemma cvg_nseries_near (u : nat^nat) : cvgn (nseries u) ->
   \forall n \near \oo, u n = 0%N.
 Proof.
 move=> /cvg_ex[l ul]; have /ul[a _ aul] : nbhs l [set l].
-  exists [set l]; split; last by split.
-  by exists [set l] => //; rewrite bigcup_set1.
+  by exists [set l]; split=> //; exists [set l] => //; rewrite bigcup_set1.
 have /ul[b _ bul] : nbhs l [set l.-1; l].
   by exists [set l]; split => //; exists [set l] => //; rewrite bigcup_set1.
 exists (maxn a b) => // n /= abn.