From fa2bfc678063419a0fdfa246f462f1629d1f69f4 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Sat, 9 Nov 2024 16:35:49 +0900 Subject: [PATCH 1/5] convergence of functions wrt deleted nbhs (#1385) * convergence of functions wrt deleted nbhs --------- Co-authored-by: IshiguroYoshihiro --- CHANGELOG_UNRELEASED.md | 2 ++ theories/realfun.v | 14 ++++++++++++++ 2 files changed, 16 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b5153bd4d..92c340e0d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -69,6 +69,8 @@ - in `measure.v`: + lemma `countable_measurable` +- in `realfun.v`: + + lemma `cvgr_dnbhsP` ### Changed diff --git a/theories/realfun.v b/theories/realfun.v index bb902bfa2..ebf570f54 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -207,6 +207,20 @@ apply: pfl. by split; [move=> k; rewrite ltrNl//|apply/cvgNP => /=; rewrite opprK]. Qed. +Lemma cvgr_dnbhsP (f : R -> R) (p l : R) : + f x @[x --> p^'] --> l <-> + (forall u : R^nat, (forall n, u n != p) /\ (u n @[n --> \oo] --> p) -> + f (u n) @[n --> \oo] --> l). +Proof. +split=> [/cvgrPdist_le fpl u [up /cvgrPdist_lt put]|pfl]. + apply/cvgrPdist_le => e /fpl [r /=] /put[n _ {}put] {}fpl. + near=> t; apply: fpl => //=; apply: put. + by near: t; exact: nbhs_infty_ge. +apply: cvg_at_right_left_dnbhs. +- by apply/cvg_at_rightP => u [pu ?]; apply: pfl; split => // n; rewrite gt_eqF. +- by apply/cvg_at_leftP => u [pu ?]; apply: pfl; split => // n; rewrite lt_eqF. +Unshelve. all: end_near. Qed. + End cvgr_fun_cvg_seq. Section cvge_fun_cvg_seq. From e792f1a37f72a65d3f6748d98bf15f141dfe6a8d Mon Sep 17 00:00:00 2001 From: zstone1 Date: Sat, 9 Nov 2024 22:51:22 -0500 Subject: [PATCH 2/5] Homeomorphisms for (X*Y)*Z -> X*(Y*Z) and X*Y -> Y*X (#1367) * homeomorphims for products --------- Co-authored-by: Reynald Affeldt --- CHANGELOG_UNRELEASED.md | 5 ++++ classical/mathcomp_extra.v | 24 ++++++++++++++++- theories/topology_theory/product_topology.v | 30 +++++++++++++++++++++ 3 files changed, 58 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 92c340e0d..d48bcd8dc 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -71,6 +71,11 @@ + lemma `countable_measurable` - in `realfun.v`: + lemma `cvgr_dnbhsP` + + new definitions `prodA`, and `prodAr`. + + new lemmas `prodAK`, `prodArK`, and `swapK`. +- in file `product_topology.v`, + + new lemmas `swap_continuous`, `prodA_continuous`, and + `prodAr_continuous`. ### Changed diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 2c72f25ca..f0ecf3733 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -18,6 +18,8 @@ From mathcomp Require Import finset interval. (* {in A &, {mono f : x y /~ x <= y}} *) (* sigT_fun f := lifts a family of functions f into a function on *) (* the dependent sum *) +(* prodA x := sends (X * Y) * Z to X * (Y * Z) *) +(* prodAr x := sends X * (Y * Z) to (X * Y) * Z *) (* ``` *) (* *) (******************************************************************************) @@ -373,7 +375,27 @@ Lemma real_ltr_distlC [R : numDomainType] [x y : R] (e : R) : x - y \is Num.real -> (`|x - y| < e) = (x - e < y < x + e). Proof. by move=> ?; rewrite distrC real_ltr_distl// -rpredN opprB. Qed. -Definition swap (T1 T2 : Type) (x : T1 * T2) := (x.2, x.1). +Definition swap {T1 T2 : Type} (x : T1 * T2) := (x.2, x.1). + +Section reassociate_products. +Context {X Y Z : Type}. + +Definition prodA (xyz : (X * Y) * Z) : X * (Y * Z) := + (xyz.1.1, (xyz.1.2, xyz.2)). + +Definition prodAr (xyz : X * (Y * Z)) : (X * Y) * Z := + ((xyz.1, xyz.2.1), xyz.2.2). + +Lemma prodAK : cancel prodA prodAr. +Proof. by case; case. Qed. + +Lemma prodArK : cancel prodAr prodA. +Proof. by case => ? []. Qed. + +End reassociate_products. + +Lemma swapK {T1 T2 : Type} : cancel (@swap T1 T2) (@swap T2 T1). +Proof. by case=> ? ?. Qed. Definition map_pair {S U : Type} (f : S -> U) (x : (S * S)) : (U * U) := (f x.1, f x.2). diff --git a/theories/topology_theory/product_topology.v b/theories/topology_theory/product_topology.v index 8e2984d35..4755458fc 100644 --- a/theories/topology_theory/product_topology.v +++ b/theories/topology_theory/product_topology.v @@ -231,3 +231,33 @@ by apply: (ngPr (b, a, i)); split => //; exact: N1N2N. Unshelve. all: by end_near. Qed. #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `compact_setX`")] Notation compact_setM := compact_setX (only parsing). + +Lemma swap_continuous {X Y : topologicalType} : continuous (@swap X Y). +Proof. +case=> a b W /= [[U V]][] /= Ub Va UVW; exists (V, U); first by split. +by case => //= ? ? [] ? ?; exact: UVW. +Qed. + +Section reassociate_continuous. +Context {X Y Z : topologicalType}. + +Lemma prodA_continuous : continuous (@prodA X Y Z). +Proof. +move=> [] [a b] c U [[/= P V]] [Pa] [][/= Q R][ Qb Rc] QRV PVU. +exists ((P `*` Q), R); first split. +- exists (P, Q); first by []. + by case=> x y /= [Px Qy]. +- by []. +- by move=> [[x y] z] [] [] ? ? ?; apply: PVU; split => //; exact: QRV. +Qed. + +Lemma prodAr_continuous : continuous (@prodAr X Y Z). +Proof. +case=> a [b c] U [[V R]] [/= [[P Q /=]]] [Pa Qb] PQV Rc VRU. +exists (P, (Q `*` R)); first split => //. +- exists (Q, R); first by []. + by case=> ? ? /= []. +- by case=> x [y z] [? [? ?]]; apply: VRU; split => //; exact: PQV. +Qed. + +End reassociate_continuous. From f5097d54c9e8afe1ac97263e943de9febb5fad7c Mon Sep 17 00:00:00 2001 From: zstone1 Date: Sun, 10 Nov 2024 09:26:18 -0500 Subject: [PATCH 3/5] Wedges part 1 (#1384) * wedges_part1 --------- Co-authored-by: Reynald Affeldt --- CHANGELOG_UNRELEASED.md | 12 ++ _CoqProject | 3 + classical/boolp.v | 7 + theories/Make | 3 + theories/homotopy_theory/homotopy.v | 2 + theories/homotopy_theory/wedge_sigT.v | 202 ++++++++++++++++++++++++++ theories/separation_axioms.v | 10 +- 7 files changed, 233 insertions(+), 6 deletions(-) create mode 100644 theories/homotopy_theory/homotopy.v create mode 100644 theories/homotopy_theory/wedge_sigT.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d48bcd8dc..4450c6f19 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -77,6 +77,18 @@ + new lemmas `swap_continuous`, `prodA_continuous`, and `prodAr_continuous`. +- file `homotopy_theory/homotopy.v` +- file `homotopy_theory/wedge_sigT.v` +- in file `homotopy_theory/wedge_sigT.v` + + new definitions `wedge_rel`, `wedge`, `wedge_lift`, `pwedge`. + + new lemmas `wedge_lift_continuous`, `wedge_lift_nbhs`, + `wedge_liftE`, `wedge_openP`, + `wedge_pointE`, `wedge_point_nbhs`, `wedge_nbhs_specP`, `wedgeTE`, + `wedge_compact`, `wedge_connected`. + +- in `boolp.`: + + lemma `existT_inj` + ### Changed - in file `normedtype.v`, diff --git a/_CoqProject b/_CoqProject index b72bbf69d..e36c71dae 100644 --- a/_CoqProject +++ b/_CoqProject @@ -61,6 +61,9 @@ theories/topology_theory/quotient_topology.v theories/topology_theory/one_point_compactification.v theories/topology_theory/sigT_topology.v +theories/homotopy_theory/homotopy.v +theories/homotopy_theory/wedge_sigT.v + theories/separation_axioms.v theories/function_spaces.v theories/ereal.v diff --git a/classical/boolp.v b/classical/boolp.v index ab36ee72c..07b4c2e09 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -88,6 +88,13 @@ move=> PQA; suff: {x | P x /\ Q x} by move=> [a [*]]; exists a. by apply: cid; case: PQA => x; exists x. Qed. +Lemma existT_inj (A : eqType) (P : A -> Type) (p : A) (x y : P p) : + existT P p x = existT P p y -> x = y. +Proof. +apply: Eqdep_dec.inj_pair2_eq_dec => a b. +by have [|/eqP] := eqVneq a b; [left|right]. +Qed. + Record mextensionality := { _ : forall (P Q : Prop), (P <-> Q) -> (P = Q); _ : forall {T U : Type} (f g : T -> U), diff --git a/theories/Make b/theories/Make index 787082052..0d77fa421 100644 --- a/theories/Make +++ b/theories/Make @@ -29,6 +29,9 @@ topology_theory/quotient_topology.v topology_theory/one_point_compactification.v topology_theory/sigT_topology.v +homotopy_theory/homotopy.v +homotopy_theory/wedge_sigT.v + separation_axioms.v function_spaces.v cantor.v diff --git a/theories/homotopy_theory/homotopy.v b/theories/homotopy_theory/homotopy.v new file mode 100644 index 000000000..33e29737b --- /dev/null +++ b/theories/homotopy_theory/homotopy.v @@ -0,0 +1,2 @@ +(* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Export wedge_sigT. diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v new file mode 100644 index 000000000..08625921f --- /dev/null +++ b/theories/homotopy_theory/wedge_sigT.v @@ -0,0 +1,202 @@ +(* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. +From mathcomp Require Import boolp classical_sets functions. +From mathcomp Require Import cardinality mathcomp_extra fsbigop. +From mathcomp Require Import reals signed topology separation_axioms. +Require Import EqdepFacts. + +(**md**************************************************************************) +(* # wedge sum for sigT *) +(* A foundational construction for homotopy theory. It glues a dependent sum *) +(* at a single point. It's classicaly used in the proof that every free group *) +(* is a fundamental group of some space. We also will use it as part of our *) +(* construction of paths and path concatenation. *) +(* ``` *) +(* wedge_rel p0 x y == x and y are equal, or they are (p0 i) and *) +(* (p0 j) for some i and j *) +(* wedge p0 == the quotient of {i : X i} along `wedge_rel p0` *) +(* wedge_lift i == the lifting of elements of (X i) into the wedge *) +(* pwedge p0 == the wedge of ptopologicalTypes at their designated *) +(* point *) +(* ``` *) +(* The type `wedge p0` is endowed with the structures of: *) +(* - topology via `quotient_topology` *) +(* - quotient *) +(* *) +(* The type `pwedge` is endowed with the structures of: *) +(* - topology via `quotient_topology` *) +(* - quotient *) +(* - pointed *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope quotient_scope. + +Section wedge. +Context {I : choiceType} (X : I -> topologicalType) (p0 : forall i, X i). +Implicit Types i : I. + +Let wedge_rel' (a b : {i & X i}) := + (a == b) || ((projT2 a == p0 _) && (projT2 b == p0 _)). + +Local Lemma wedge_rel_refl : reflexive wedge_rel'. +Proof. by move=> ?; rewrite /wedge_rel' eqxx. Qed. + +Local Lemma wedge_rel_sym : symmetric wedge_rel'. +Proof. +by move=> a b; apply/is_true_inj/propext; rewrite /wedge_rel'; split; + rewrite (eq_sym b) andbC. +Qed. + +Local Lemma wedge_rel_trans : transitive wedge_rel'. +Proof. +move=> a b c /predU1P[-> //|] + /predU1P[<- //|]; rewrite /wedge_rel'. +by move=> /andP[/eqP -> /eqP <-] /andP[_ /eqP <-]; rewrite !eqxx orbC. +Qed. + +Definition wedge_rel := EquivRel _ wedge_rel_refl wedge_rel_sym wedge_rel_trans. +Global Opaque wedge_rel. + +Definition wedge := {eq_quot wedge_rel}. +Definition wedge_lift i : X i -> wedge := \pi_wedge \o existT X i. + +HB.instance Definition _ := Topological.copy wedge (quotient_topology wedge). +HB.instance Definition _ := Quotient.on wedge. +Global Opaque wedge. + +Lemma wedge_lift_continuous i : continuous (@wedge_lift i). +Proof. by move=> ?; apply: continuous_comp => //; exact: pi_continuous. Qed. + +HB.instance Definition _ i := + @isContinuous.Build _ _ (@wedge_lift i) (@wedge_lift_continuous i). + +Lemma wedge_lift_nbhs i (x : X i) : + closed [set p0 i] -> x != p0 _ -> @wedge_lift i @ x = nbhs (@wedge_lift _ x). +Proof. +move=> clx0 xNx0; rewrite eqEsubset; split => U; first last. + by move=> ?; exact: wedge_lift_continuous. +rewrite ?nbhsE /= => -[V [oV Vx VU]]. +exists (@wedge_lift i @` (V `&` ~` [set p0 i])); first last. + by move=> ? /= [l] [Vl lx] <-; exact: VU. +split; last by exists x => //; split => //=; exact/eqP. +rewrite /open /= /quotient_open /wedge_lift /=. +suff -> : \pi_wedge @^-1` (@wedge_lift i @` (V `&` ~`[set p0 i])) = + existT X i @` (V `&` ~` [set p0 i]). + by apply: existT_open_map; apply: openI => //; exact: closed_openC. +rewrite eqEsubset; split => t /= [l [Vl] lNx0]; last by move=> <-; exists l. +by case/eqmodP/predU1P => [<-|/andP [/eqP]//]; exists l. +Qed. + +Lemma wedge_liftE i (x : X i) j (y : X j) : + wedge_lift (p0 j) = wedge_lift (p0 i). +Proof. by apply/eqmodP/orP; right; rewrite !eqxx. Qed. + +Lemma wedge_openP (U : set wedge) : + open U <-> forall i, open (@wedge_lift i @^-1` U). +Proof. +split=> [oU i|oiU]. + by apply: open_comp => // x _; exact: wedge_lift_continuous. +have : open (\bigcup_i (@wedge_lift i @` (@wedge_lift i @^-1` U))). + apply/sigT_openP => i; move: (oiU i); congr open. + rewrite eqEsubset; split => x /=. + by move=> Ux; exists i => //; exists x. + case=> j _ /= [] y Uy /eqmodP /predU1P[R|]. + have E : j = i by move: R; exact: eq_sigT_fst. + by rewrite -E in x R *; rewrite -(existT_inj R). + case/andP => /eqP/= + /eqP -> => yj. + by rewrite yj (wedge_liftE x y) in Uy. +congr open; rewrite eqEsubset; split => /= z. + by case=> i _ /= [x] Ux <-. +move=> Uz; exists (projT1 (repr z)) => //=. +by exists (projT2 (repr z)); rewrite /wedge_lift /= -sigT_eta reprK. +Qed. + +Lemma wedge_point_nbhs i0 : + nbhs (wedge_lift (p0 i0)) = \bigcap_i (@wedge_lift i @ p0 i). +Proof. +rewrite eqEsubset; split => //= U /=; rewrite ?nbhs_simpl. + case=> V [/= oV Vp] VU j _; apply: wedge_lift_continuous. + apply: (filterS VU); first exact: (@nbhs_filter wedge). + apply: open_nbhs_nbhs; split => //. + by rewrite (wedge_liftE (p0 i0)). +move=> Uj; have V_ : forall i, {V : set (X i) | + [/\ open V, V (p0 i) & V `<=` @wedge_lift i @^-1` U]}. + move=> j; apply: cid; have /Uj : [set: I] j by []. + by rewrite nbhsE /= => -[B [? ? ?]]; exists B. +pose W := \bigcup_i (@wedge_lift i) @` (projT1 (V_ i)). +exists W; split. +- apply/wedge_openP => i; rewrite /W; have [+ Vpj _] := projT2 (V_ i). + congr (_ _); rewrite eqEsubset; split => z; first by move=> Viz; exists i. + case => j _ /= [] w /= svw /eqmodP /predU1P[[E]|]. + by rewrite E in w svw * => R; rewrite -(existT_inj R). + by case/andP => /eqP /= _ /eqP ->. +- by exists i0 => //=; exists (p0 i0) => //; have [_ + _] := projT2 (V_ i0). +- by move=> ? [j _ [x ? <-]]; have [_ _] := projT2 (V_ j); exact. +Qed. + +Variant wedge_nbhs_spec (z : wedge) : wedge -> set_system wedge -> Type := + | wedge_liftsPoint i0 : + wedge_nbhs_spec z (wedge_lift (p0 i0)) (\bigcap_i (@wedge_lift i @ p0 i)) + | WedgeNotPoint (i : I) (x : X i) of (x != p0 i): + wedge_nbhs_spec z (wedge_lift x) (@wedge_lift i @ x). + +Lemma wedge_nbhs_specP (z : wedge) : (forall i, closed [set p0 i]) -> + wedge_nbhs_spec z z (nbhs z). +Proof. +move=> clP; rewrite -[z](@reprK _ wedge); case: (repr z) => i x. +have [->|xpi] := eqVneq x (p0 i). + by rewrite wedge_point_nbhs => /=; exact: wedge_liftsPoint. +by rewrite /= -wedge_lift_nbhs //; exact: WedgeNotPoint. +Qed. + +Lemma wedgeTE : \bigcup_i (@wedge_lift i) @` setT = [set: wedge]. +Proof. +rewrite -subTset => z _; rewrite -[z]reprK; exists (projT1 (repr z)) => //. +by exists (projT2 (repr z)) => //; rewrite /wedge_lift/= -sigT_eta. +Qed. + +Lemma wedge_compact : finite_set [set: I] -> (forall i, compact [set: X i]) -> + compact [set: wedge]. +Proof. +move=> fsetI cptX; rewrite -wedgeTE -fsbig_setU //; apply: big_ind. +- exact: compact0. +- by move=> ? ? ? ?; exact: compactU. +move=> i _; apply: continuous_compact; last exact: cptX. +exact/continuous_subspaceT/wedge_lift_continuous. +Qed. + +Lemma wedge_connected : (forall i, connected [set: X i]) -> + connected [set: wedge]. +Proof. +move=> ctdX; rewrite -wedgeTE. +have [I0|/set0P[i0 Ii0]] := eqVneq [set: I] set0. + rewrite [X in connected X](_ : _ = set0); first exact: connected0. + by rewrite I0 bigcup_set0. +apply: bigcup_connected. + exists (@wedge_lift i0 (p0 _)) => i Ii; exists (p0 i) => //. + exact: wedge_liftE. +move=> i ? /=; apply: connected_continuous_connected => //. +exact/continuous_subspaceT/wedge_lift_continuous. +Qed. + +End wedge. + +Section pwedge. +Context {I : pointedType} (X : I -> ptopologicalType). + +Definition pwedge := wedge (fun i => @point (X i)). + +Let pwedge_point : pwedge := wedge_lift _ (@point (X (@point I))). + +HB.instance Definition _ := Topological.on pwedge. +HB.instance Definition _ := Quotient.on pwedge. +HB.instance Definition _ := isPointed.Build pwedge pwedge_point. + +End pwedge. diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v index ff6f7702c..afd1f4ad6 100644 --- a/theories/separation_axioms.v +++ b/theories/separation_axioms.v @@ -1114,12 +1114,11 @@ Lemma perfectTP_ex {T} : perfect_set [set: T] <-> forall (U : set T), open U -> U !=set0 -> exists x y, [/\ U x, U y & x != y] . Proof. -apply: iff_trans; first exact: perfectTP; split. +apply: (iff_trans perfectTP); split. move=> nx1 U oU [] x Ux; exists x. have : U <> [set x] by move=> Ux1; apply: (nx1 x); rewrite -Ux1. - apply: contra_notP; move/not_existsP/contrapT=> Uyx; rewrite eqEsubset. - (split => //; last by move=> ? ->); move=> y Uy; have /not_and3P := Uyx y. - by case => // /negP; rewrite negbK => /eqP ->. + apply: contra_notP => /not_existsP/contrapT=> Uyx; rewrite eqEsubset. + by split => [y Uy|? ->//]; have /not_and3P[//|//|/negP/negPn/eqP] := Uyx y. move=> Unxy x Ox; have [] := Unxy _ Ox; first by exists x. by move=> y [] ? [->] -> /eqP. Qed. @@ -1140,8 +1139,7 @@ rewrite {}ji {j} in x y cl *. congr existT; apply: hX => U V Ux Vy. have [] := cl (existT X i @` U) (existT X i @` V); [exact: existT_nbhs..|]. move=> z [] [l Ul <-] [r Vr lr]; exists l; split => //. -rewrite (Eqdep_dec.inj_pair2_eq_dec _ _ _ _ _ _ lr)// in Vr. -by move=> a b; exact: pselect. +by rewrite -(existT_inj lr). Qed. End sigT_separations. From 7e2988da66a63c991b612ce0fd9d7af2513b5941 Mon Sep 17 00:00:00 2001 From: zstone1 Date: Sun, 10 Nov 2024 10:09:29 -0500 Subject: [PATCH 4/5] min and max are continuous (#1387) * min and max are continuous --------- Co-authored-by: Reynald Affeldt --- CHANGELOG_UNRELEASED.md | 3 + theories/topology_theory/order_topology.v | 78 ++++++++++++++++++++++- 2 files changed, 80 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4450c6f19..260152313 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -88,6 +88,9 @@ - in `boolp.`: + lemma `existT_inj` +- in file `order_topology.v` + + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and + `max_fun_continuous`. ### Changed diff --git a/theories/topology_theory/order_topology.v b/theories/topology_theory/order_topology.v index a959bff76..99df6a824 100644 --- a/theories/topology_theory/order_topology.v +++ b/theories/topology_theory/order_topology.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap all_classical. From mathcomp Require Import topology_structure uniform_structure. -From mathcomp Require Import pseudometric_structure. +From mathcomp Require Import product_topology pseudometric_structure. (**md**************************************************************************) (* # Order topology *) @@ -220,3 +220,79 @@ Qed. HB.instance Definition _ := Order_isNbhs.Build _ oT order_nbhs_itv. End induced_order_topology. + +Lemma min_continuous {d} {T : orderTopologicalType d} : + continuous (fun xy : T * T => Order.min xy.1 xy.2). +Proof. +case=> x y; have [<- U /=|]:= eqVneq x y. + rewrite min_l// => Ux; exists (U, U) => //= -[a b [Ua Ub]]. + by have /orP[?|?]/= := le_total a b; [rewrite min_l|rewrite min_r]. +wlog xy : x y / (x < y)%O. + move=> WH /[dup] /lt_total/orP[|yx /eqP/nesym/eqP yNx]; first exact: WH. + rewrite (_ : (fun _ => _) = (fun xy => Order.min xy.1 xy.2) \o @swap T T). + by apply: continuous_comp; [exact: swap_continuous|exact: WH]. + apply/funext => -[a b/=]; have /orP[ab|ba] := le_total a b. + - by rewrite min_l // min_r. + - by rewrite min_r // min_l. +move=> _ U /=; rewrite (min_l (ltW xy)) => Ux. +have [[z xzy]|/forallNP/= xNy] := pselect (exists z, x < z < y)%O. + exists (U `&` `]-oo, z[, `]z, +oo[%classic) => /=. + split; [apply: filterI =>//|]; apply: open_nbhs_nbhs. + - by split; [exact: lray_open|rewrite set_itvE; case/andP: xzy]. + - by split; [exact: rray_open|rewrite set_itvE; case/andP: xzy]. + case=> a b /= [[Ua]]; rewrite !in_itv andbT /= => az zb. + by rewrite min_l// (ltW (lt_trans az _)). +exists (U `&` `]-oo, y[, `]x, +oo[%classic) => /=. + split; [apply: filterI => //|]; apply: open_nbhs_nbhs. + - by split; [exact: lray_open|rewrite set_itvE]. + - by split; [exact: rray_open|rewrite set_itvE]. +case=> a b /= [[Ua]]; rewrite !in_itv andbT /= => ay xb. +rewrite min_l// leNgt; apply: contra_notN (xNy b) => ba. +by rewrite xb (lt_trans ba). +Qed. + +Lemma min_fun_continuous {d} {X : topologicalType} {T : orderTopologicalType d} + (f g : X -> T) : + continuous f -> continuous g -> continuous (f \min g). +Proof. +move=> fc gc z; apply: continuous2_cvg; [|exact: fc|exact: gc]. +by apply min_continuous. +Qed. + +Lemma max_continuous {d} {T : orderTopologicalType d} : + continuous (fun xy : T * T => Order.max xy.1 xy.2). +Proof. +case=> x y; have [<- U|] := eqVneq x y. + rewrite /= max_r // => ux; exists (U, U) => //= -[a b] [/= Ua Ub]. + by have /orP[?|?]/= := le_total a b; [rewrite max_r|rewrite max_l]. +wlog xy : x y / (x < y)%O. + move=> WH /[dup] /lt_total/orP[|yx /eqP/nesym/eqP yNx]; first exact: WH. + rewrite (_ : (fun _ => _) = (fun xy => Order.max xy.1 xy.2) \o @swap T T). + by apply: continuous_comp; [exact: swap_continuous|exact: WH]. + apply/funext => -[a b] /=; have /orP [ab|ba] := le_total a b. + - by rewrite max_r // max_l. + - by rewrite max_l // max_r. +move=> _ U /=; rewrite (max_r (ltW xy)) => Ux. +have [[z xzy]|/forallNP /= xNy] := pselect (exists z, x < z < y)%O. + exists (`]-oo, z[%classic, U `&` `]z, +oo[) => /=. + split; [|apply: filterI =>//]; apply: open_nbhs_nbhs. + - by split; [exact: lray_open|rewrite set_itvE; case/andP: xzy]. + - by split; [exact: rray_open|rewrite set_itvE; case/andP: xzy]. + case=> a b /= [] + []; rewrite !in_itv andbT /= => az Ub zb. + by rewrite (max_r (ltW (lt_trans az _))). +exists (`]-oo, y[%classic, U `&` `]x, +oo[) => /=. + split; [|apply: filterI => //]; apply: open_nbhs_nbhs. + - by split; [exact: lray_open|rewrite set_itvE]. + - by split; [exact: rray_open|rewrite set_itvE]. +case=> a b /=; rewrite !in_itv /= andbT => [/=] [ay] [Ub] xb. +rewrite max_r// leNgt; apply: contra_notN (xNy b) => ba. +by rewrite xb (lt_trans ba). +Qed. + +Lemma max_fun_continuous {d} {X : topologicalType} {T : orderTopologicalType d} + (f g : X -> T): + continuous f -> continuous g -> continuous (f \max g). +Proof. +move=> fc gc z; apply: continuous2_cvg; [|exact: fc|exact: gc]. +by apply max_continuous. +Qed. From b74a117092059a3ffb9be9b5e56b6013fb03e477 Mon Sep 17 00:00:00 2001 From: IshYosh <103252572+IshiguroYoshihiro@users.noreply.github.com> Date: Wed, 13 Nov 2024 19:22:29 +0900 Subject: [PATCH 5/5] near_in_itv_oy/Nyo (#1375) * near_in_itv_oy/Nyo --------- Co-authored-by: Reynald Affeldt --- CHANGELOG_UNRELEASED.md | 4 ++++ theories/ftc.v | 2 +- theories/normedtype.v | 38 +++++++++++++++++++++++++++++++++++--- theories/realfun.v | 4 ++-- theories/trigo.v | 12 ++++++------ 5 files changed, 48 insertions(+), 12 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 260152313..a191ece6d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -56,6 +56,7 @@ `nbhs_one_point_compactification_weakE`, `locally_compact_completely_regular`, and `completely_regular_regular`. + + new lemmas `near_in_itvoy`, `near_in_itvNyo` - in file `mathcomp_extra.v`, + new definition `sigT_fun`. @@ -147,6 +148,9 @@ ### Renamed +- in `normedtype.v`: + + `near_in_itv` -> `near_in_itvoo` + ### Generalized - in `lebesgue_integral.v`: diff --git a/theories/ftc.v b/theories/ftc.v index 4f553f2c1..7be07799d 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -979,7 +979,7 @@ rewrite (@integration_by_substitution_decreasing (- F)%R); first last. rewrite -derive1E. have /cvgN := cF' _ xab; apply: cvg_trans; apply: near_eq_cvg. rewrite near_simpl; near=> y; rewrite fctE !derive1E deriveN//. - by case: Fab => + _ _; apply; near: y; exact: near_in_itv. + by case: Fab => + _ _; apply; near: y; exact: near_in_itvoo. - by move=> x y xab yab yx; rewrite ltrN2 incrF. - by []. have mGF : measurable_fun `]a, b[ (G \o F). diff --git a/theories/normedtype.v b/theories/normedtype.v index debaf7d26..8d0fc8437 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -5336,10 +5336,42 @@ Lemma bound_itvE (R : numDomainType) (a b : R) : (a \in `]-oo, a]). Proof. by rewrite !(boundr_in_itv, boundl_in_itv). Qed. -Lemma near_in_itv {R : realFieldType} (a b : R) : +Section near_in_itv. +Context {R : realFieldType} (a b : R). + +Lemma near_in_itvoo : {in `]a, b[, forall y, \forall z \near y, z \in `]a, b[}. Proof. exact: interval_open. Qed. +Lemma near_in_itvoy : + {in `]a, +oo[, forall y, \forall z \near y, z \in `]a, +oo[}. +Proof. +move=> x ax. +near=> z. +suff : z \in `]a, +oo[%classic by rewrite inE. +near: z. +rewrite near_nbhs. +apply: (@open_in_nearW _ _ `]a, +oo[%classic) => //. +by rewrite inE. +Unshelve. end_near. Qed. + +Lemma near_in_itvNyo : + {in `]-oo, b[, forall y, \forall z \near y, z \in `]-oo, b[}. +Proof. +move=> x xb. +near=> z. +suff : z \in `]-oo, b[%classic by rewrite inE. +near: z. +rewrite near_nbhs. +apply: (@open_in_nearW _ _ `]-oo, b[%classic) => //. +by rewrite inE/=. +Unshelve. end_near. Qed. + +End near_in_itv. +#[deprecated(since="mathcomp-analysis 1.7.0", + note="use `near_in_itvoo` instead")] +Notation near_in_itv := near_in_itvoo (only parsing). + Lemma cvg_patch {R : realType} (f : R -> R^o) (a b : R) (x : R) : (a < b)%R -> x \in `]a, b[ -> f @ (x : subspace `[a, b]) --> f x -> @@ -5350,7 +5382,7 @@ move/cvgrPdist_lt : xf => /(_ e e0) xf. near=> z. rewrite patchE ifT//; last first. rewrite inE; apply: subset_itv_oo_cc. - by near: z; exact: near_in_itv. + by near: z; exact: near_in_itvoo. near: z. rewrite /prop_near1 /nbhs/= /nbhs_subspace ifT// in xf; last first. by rewrite inE/=; exact: subset_itv_oo_cc xab. @@ -5358,7 +5390,7 @@ case: xf => x0 /= x00 xf. near=> z. apply: xf => //=. rewrite inE; apply: subset_itv_oo_cc. -by near: z; exact: near_in_itv. +by near: z; exact: near_in_itvoo. Unshelve. all: by end_near. Qed. Notation "f @`[ a , b ]" := diff --git a/theories/realfun.v b/theories/realfun.v index ebf570f54..70fae9c30 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1435,10 +1435,10 @@ have := xb; rewrite le_eqVlt => /orP[/eqP {}xb {ax}|{}xb]. have xoab : x \in `]a, b[ by rewrite in_itv /=; apply/andP; split. near=> y; suff: l <= f y <= u. by rewrite ge_max le_min -!andbA => /and4P[-> _ ->]. -have ? : y \in `[a, b] by apply: subset_itv_oo_cc; near: y; apply: near_in_itv. +have ? : y \in `[a, b] by apply: subset_itv_oo_cc; near: y; exact: near_in_itvoo. have fyab : f y \in `[f a, f b] by rewrite in_itv/= !fle// ?ltW. rewrite -[l <= _]gle -?[_ <= u]gle// ?fK //. -apply: subset_itv_oo_cc; near: y; apply: near_in_itv; rewrite in_itv /=. +apply: subset_itv_oo_cc; near: y; apply: near_in_itvoo; rewrite in_itv /=. rewrite -[x]fK // !glt//= lt_min gt_max ?andbT ltrBlDr ltr_pwDr //. by apply/and3P; split; rewrite // flt. Unshelve. all: by end_near. Qed. diff --git a/theories/trigo.v b/theories/trigo.v index cfcd3db86..39bebecc9 100644 --- a/theories/trigo.v +++ b/theories/trigo.v @@ -1003,7 +1003,7 @@ move=> /andP[x_gtN1 x_lt1]; rewrite -[x]acosK; first last. by have : -1 <= x <= 1 by rewrite !ltW //; case/andP: xB. apply: nbhs_singleton (near_can_continuous _ _); last first. by near=> z; apply: continuous_cos. -have /near_in_itv aI : acos x \in `]0, pi[. +have /near_in_itvoo aI : acos x \in `]0, pi[. suff : 0 < acos x < pi by []. by rewrite acos_gt0 ?ltW //= acos_ltpi // ltW ?andbT. near=> z; apply: cosK. @@ -1016,7 +1016,7 @@ Lemma is_derive1_acos x : Proof. move=> /andP[x_gtN1 x_lt1]; rewrite -sin_acos ?ltW // -invrN. rewrite -{1}[x]acosK; last by have : -1 <= x <= 1 by rewrite ltW // ltW. -have /near_in_itv aI : acos x \in `]0, pi[. +have /near_in_itvoo aI : acos x \in `]0, pi[. suff : 0 < acos x < pi by []. by rewrite acos_gt0 ?ltW //= acos_ltpi // ltW ?andbT. apply: (@is_derive_inverse R cos). @@ -1103,7 +1103,7 @@ move=> /andP[x_gtN1 x_lt1]; rewrite -[x]asinK; first last. by have : -1 <= x <= 1 by rewrite !ltW //; case/andP: xB. apply: nbhs_singleton (near_can_continuous _ _); last first. by near=> z; apply: continuous_sin. -have /near_in_itv aI : asin x \in `](-(pi/2)), (pi/2)[. +have /near_in_itvoo aI : asin x \in `](-(pi/2)), (pi/2)[. suff : - (pi / 2) < asin x < pi / 2 by []. by rewrite asin_gtNpi2 ?ltW ?andbT //= asin_ltpi2 // ltW. near=> z; apply: sinK. @@ -1117,7 +1117,7 @@ Lemma is_derive1_asin x : Proof. move=> /andP[x_gtN1 x_lt1]; rewrite -cos_asin ?ltW //. rewrite -{1}[x]asinK; last by have : -1 <= x <= 1 by rewrite ltW // ltW. -have /near_in_itv aI : asin x \in `](-(pi/2)), (pi/2)[. +have /near_in_itvoo aI : asin x \in `](-(pi/2)), (pi/2)[. suff : -(pi/2) < asin x < pi/2 by []. by rewrite asin_gtNpi2 ?ltW ?andbT //= asin_ltpi2 // ltW. apply: (@is_derive_inverse R sin). @@ -1219,7 +1219,7 @@ Qed. Lemma continuous_atan x : {for x, continuous (@atan R)}. Proof. rewrite -[x]atanK. -have /near_in_itv aI : atan x \in `](-(pi / 2)), (pi / 2)[. +have /near_in_itvoo aI : atan x \in `](-(pi / 2)), (pi / 2)[. suff : - (pi / 2) < atan x < pi / 2 by []. by rewrite atan_gtNpi2 atan_ltpi2. apply: nbhs_singleton (near_can_continuous _ _); last first. @@ -1244,7 +1244,7 @@ Proof. rewrite -{1}[x]atanK. have cosD0 : cos (atan x) != 0. by apply/lt0r_neq0/cos_gt0_pihalf; rewrite atan_gtNpi2 atan_ltpi2. -have /near_in_itv aI : atan x \in `](-(pi/2)), (pi/2)[. +have /near_in_itvoo aI : atan x \in `](-(pi/2)), (pi/2)[. suff : - (pi / 2) < atan x < pi / 2 by []. by rewrite atan_gtNpi2 atan_ltpi2. apply: (@is_derive_inverse R tan).