diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 45d3a8fa1..acacf8db1 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,72 +4,11 @@ ### Added -- file `Rstruct_topology.v` - -- package `coq-mathcomp-reals` depending on `coq-mathcomp-classical` - with files - + `constructive_ereal.v` - + `reals.v` - + `real_interval.v` - + `signed.v` - + `itv.v` - + `prodnormedzmodule.v` - + `nsatz_realtype.v` - + `all_reals.v` - -- in file `separation_axioms.v`, - + new lemmas `compact_normal_local`, and `compact_normal`. - -- package `coq-mathcomp-altreals` depending on `coq-mathcomp-reals` - with files - + `xfinmap.v` - + `discrete.v` - + `realseq.v` - + `realsum.v` - + `distr.v` - -- package `coq-mathcomp-reals-stdlib` depending on `coq-mathcomp-reals` - with file - + `Rstruct.v` - -- package `coq-mathcomp-analysis-stdlib` depending on - `coq-mathcomp-analysis` and `coq-mathcomp-reals-stdlib` with files - + `Rstruct_topology.v` - + `showcase/uniform_bigO.v` - -- in file `separation_axioms.v`, - + new lemmas `compact_normal_local`, and `compact_normal`. - -- in file `topology_theory/one_point_compactification.v`, - + new definitions `one_point_compactification`, and `one_point_nbhs`. - + new lemmas `one_point_compactification_compact`, - `one_point_compactification_some_nbhs`, - `one_point_compactification_some_continuous`, - `one_point_compactification_open_some`, - `one_point_compactification_weak_topology`, and - `one_point_compactification_hausdorff`. - -- in file `normedtype.v`, - + new definition `type` (in module `completely_regular_uniformity`) - + new lemmas `normal_completely_regular`, - `one_point_compactification_completely_reg`, - `nbhs_one_point_compactification_weakE`, - `locally_compact_completely_regular`, and - `completely_regular_regular`. - -- in file `mathcomp_extra.v`, - + new definition `sigT_fun`. -- in file `sigT_topology.v`, - + new definition `sigT_nbhs`. - + new lemmas `sigT_nbhsE`, `existT_continuous`, `existT_open_map`, - `existT_nbhs`, `sigT_openP`, `sigT_continuous`, `sigT_setUE`, and - `sigT_compact`. -- in file `separation_axioms.v`, - + new lemma `sigT_hausdorff`. +- in `num_topology.v`: + + lemma `in_continuous_mksetP` - in `normedtype.v`: - + lemma `in_continuous_mksetP` - + lemmas `continuous_within_itvcyP`, `continuous_within_itvycP` + + lemmas `continuous_within_itvcyP`, `continuous_within_itvNycP` ### Changed diff --git a/theories/normedtype.v b/theories/normedtype.v index c432bb377..46eba5707 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -8,7 +8,6 @@ From mathcomp Require Import cardinality set_interval ereal reals. From mathcomp Require Import signed topology prodnormedzmodule function_spaces. From mathcomp Require Export real_interval separation_axioms tvs. - (**md**************************************************************************) (* # Norm-related Notions *) (* *) @@ -2158,14 +2157,6 @@ by apply: xe_A => //; rewrite eq_sym. Qed. Arguments cvg_at_leftE {R V} f x. -(* TODO: move earlier *) -Lemma in_continuous_mksetP {T : realFieldType} {U : realFieldType} - (i : interval T) (f : T -> U) : - {in i, continuous f} <-> {in [set` i], continuous f}. -Proof. -by split => [fi x /set_mem/=|fi x xi]; [exact: fi|apply: fi; rewrite inE]. -Qed. - Section continuous_within_itvP. Context {R : realType}. Implicit Type f : R -> R. @@ -2259,7 +2250,7 @@ rewrite bnd_simp/= le_eqVlt => /predU1P[<-{x}|ax] _. by move=> ?/=; rewrite !in_itv/= !andbT; exact: ltW. Qed. -Lemma continuous_within_itvycP b (f : R -> R) : +Lemma continuous_within_itvNycP b (f : R -> R) : {within `]-oo, b], continuous f} <-> {in `]-oo, b[, continuous f} /\ f x @[x --> b^'-] --> f b. Proof. diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v index ea87ef618..c56d7512f 100644 --- a/theories/topology_theory/num_topology.v +++ b/theories/topology_theory/num_topology.v @@ -90,6 +90,13 @@ End numFieldTopology. Import numFieldTopology.Exports. +Lemma in_continuous_mksetP {T : realFieldType} {U : realFieldType} + (i : interval T) (f : T -> U) : + {in i, continuous f} <-> {in [set` i], continuous f}. +Proof. +by split => [fi x /set_mem/=|fi x xi]; [exact: fi|apply: fi; rewrite inE]. +Qed. + Lemma nbhs0_ltW (R : realFieldType) (x : R) : (0 < x)%R -> \forall r \near nbhs (0%R:R), (r <= x)%R. Proof.