Skip to content

Commit

Permalink
doc, trailing spaces
Browse files Browse the repository at this point in the history
  • Loading branch information
@affeldt-aist
affeldt-aist committed Jan 10, 2025
1 parent 7346645 commit 2e448c5
Show file tree
Hide file tree
Showing 2 changed files with 47 additions and 135 deletions.
114 changes: 4 additions & 110 deletions CHANGELOG_UNRELEASED.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,105 +14,6 @@
+ lemmas `horner0_ext`, `hornerD_ext`, `horner_scale_ext`, `hornerC_ext`,
`derivable_horner`, `derivE`, `continuous_horner`
+ instance `is_derive_poly`
- in file `separation_axioms.v`,
+ new lemmas `compact_normal_local`, and `compact_normal`.

- package `coq-mathcomp-experimental-reals` 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`.
+ new lemmas `near_in_itvoy`, `near_in_itvNyo`

- 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 `measure.v`:
+ 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`.

- 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`
- in file `order_topology.v`
+ new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and
`max_fun_continuous`.

- in file `bool_topology.v`,
+ new lemma `bool_compact`.

### Changed

- in file `normedtype.v`,
changed `completely_regular_space` to depend on uniform separators
which removes the dependency on `R`. The old formulation can be
recovered easily with `uniform_separatorP`.

- moved from `Rstruct.v` to `Rstruct_topology.v`
+ lemmas `continuity_pt_nbhs`, `continuity_pt_cvg`,
`continuity_ptE`, `continuity_pt_cvg'`, `continuity_pt_dnbhs`
and `nbhs_pt_comp`

- moved from `real_interval.v` to `normedtype.v`
+ lemmas `set_itvK`, `RhullT`, `RhullK`, `set_itv_setT`,
`Rhull_smallest`, `le_Rhull`, `neitv_Rhull`, `Rhull_involutive`,
`disj_itv_Rhull`
- in `topology.v`:
+ lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`,
`subspace_pm_ball_triangle`, `subspace_pm_entourage` turned
into local `Let`'s

- in `lebesgue_integral.v`:
+ lemmas `integral_fin_num_abs`, `Rintegral_cst`, `le_Rintegral`
Expand All @@ -129,6 +30,9 @@
- in `classical_sets.v`:
+ lemmas `xsectionE`, `ysectionE`

- in file `bool_topology.v`,
+ new lemma `bool_compact`.

### Changed

- in `lebesgue_integrale.v`
Expand All @@ -142,12 +46,12 @@

- moved from `lebesgue_integral.v` to `measure.v` and generalized
+ lemmas `measurable_xsection`, `measurable_ysection`

- moved from `topology_structure.v` to `discrete_topology.v`:
`discrete_open`, `discrete_set1`, `discrete_closed`, and `discrete_cvg`.

- moved from `pseudometric_structure.v` to `discrete_topology.v`:
`discrete_ent`, `discrete_ball`, and `discrete_topology`.

- in file `cantor.v`, `cantor_space` now defined in terms of `bool`.
- in file `separation_axioms.v`, updated `discrete_hausdorff`, and
`discrete_zero_dimension` to take a `discreteTopologicalType`.
Expand Down Expand Up @@ -184,17 +88,7 @@
- in `sequences.v`:
+ notations `nneseries_pred0`, `eq_nneseries`, `nneseries0`,
`ereal_cvgPpinfty`, `ereal_cvgPninfty` (were deprecated since 0.6.0)
- in `lebesgue_integral.v`:
+ definition `cst_mfun`
+ lemma `mfun_cst`

- in `cardinality.v`:
+ lemma `cst_fimfun_subproof`

- in `lebesgue_integral.v`:
+ lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead)
+ lemma `cst_nnfun_subproof` (turned into a `Let`)
+ lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead)
- in file `topology_structure.v`, removed `discrete_sing`, `discrete_nbhs`, and `discrete_space`.
- in file `nat_topology.v`, removed `discrete_nat`.
- in file `pseudometric_structure.v`, removed `discrete_ball_center`, `discrete_topology_type`, and
Expand Down
68 changes: 43 additions & 25 deletions theories/topology_theory/discrete_topology.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,58 +3,76 @@ From mathcomp Require Import all_ssreflect all_algebra all_classical all_reals.
From mathcomp Require Import topology_structure uniform_structure.
From mathcomp Require Import order_topology pseudometric_structure compact.

(**md**************************************************************************)
(* # Discrete Topology *)
(* ``` *)
(* discreteNbhsType == neighborhoods are principal filters *)
(* discrete_ent == entourages of the discrete uniformity *)
(* topology, equipped with the Uniform *)
(* structure *)
(* discrete_ball == singleton balls for the discrete metric, *)
(* equipped with the Uniform structure *)
(* discreteTopologicalType == types with a discrete topology *)
(* discreteOrderTopologicalType == *)
(* pdiscreteTopologicalType == *)
(* pdiscreteOrderTopologicalType == *)
(* discreteUniformType == *)
(* discretePseudoMetricType == *)
(* discrete_topology T == alias attaching discrete structures for *)
(* topology, uniformity, and pseudometric *)
(* ``` *)
(******************************************************************************)
Import Order.TTheory GRing.Theory Num.Def Num.Theory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.


HB.mixin Record Discrete_ofNbhs T of Nbhs T := {
nbhs_principalE : (@nbhs T _) = principal_filter;
}.

#[short(type="discreteNbhsType")]
HB.structure Definition DiscreteNbhs := {T of Nbhs T & Discrete_ofNbhs T}.


Definition discrete_ent {T} : set (set (T * T)) :=
globally (range (fun x => (x, x))).

(** Note: having the discrete topology does not guarantee the discrete
(** Note: having the discrete topology does not guarantee the discrete
uniformity. Likewise for the discrete metric. Consider [set 1/n | n in R] *)
HB.mixin Record Discrete_ofUniform T of Uniform T := {
uniform_discrete : @entourage T = discrete_ent
}.

Definition discrete_ball {R : numDomainType} {T} (x : T) (eps : R) y : Prop := x = y.
Definition discrete_ball {R : numDomainType} {T} (x : T) (eps : R) y : Prop :=
x = y.

HB.mixin Record Discrete_ofPseudometric {R : numDomainType} T of
HB.mixin Record Discrete_ofPseudometric {R : numDomainType} T of
PseudoMetric R T := {
metric_discrete : @ball R T = @discrete_ball R T
}.

#[short(type="discreteTopologicalType")]
HB.structure Definition DiscreteTopology :=
HB.structure Definition DiscreteTopology :=
{ T of DiscreteNbhs T & Topological T}.

#[short(type="discreteOrderTopologicalType")]
HB.structure Definition DiscreteOrderTopology d :=
HB.structure Definition DiscreteOrderTopology d :=
{ T of Discrete_ofNbhs T & OrderTopological d T}.

#[short(type="pdiscreteTopologicalType")]
HB.structure Definition PointedDiscreteTopology :=
HB.structure Definition PointedDiscreteTopology :=
{ T of DiscreteTopology T & Pointed T}.

#[short(type="pdiscreteOrderTopologicalType")]
HB.structure Definition PointedDiscreteOrderTopology d :=
HB.structure Definition PointedDiscreteOrderTopology d :=
{ T of Discrete_ofNbhs T & OrderTopological d T & Pointed T}.

#[short(type="discreteUniformType")]
HB.structure Definition DiscreteUniform :=
HB.structure Definition DiscreteUniform :=
{ T of Discrete_ofUniform T & Uniform T & Discrete_ofNbhs T}.

#[short(type="discretePseudoMetricType")]
HB.structure Definition DiscretePseudoMetric {R : numDomainType} :=
HB.structure Definition DiscretePseudoMetric {R : numDomainType} :=
{ T of Discrete_ofPseudometric R T & PseudoMetric R T & DiscreteUniform T}.

HB.builders Context T of Discrete_ofNbhs T.
Expand All @@ -65,7 +83,8 @@ Proof. rewrite nbhs_principalE; exact: principal_filter_proper. Qed.
Local Lemma principal_nbhs_singleton (p : T) (A : set T) : nbhs p A -> A p.
Proof. by rewrite nbhs_principalE => /principal_filterP. Qed.

Local Lemma principal_nbhs_nbhs (p : T) (A : set T) : nbhs p A -> nbhs p (nbhs^~ A).
Local Lemma principal_nbhs_nbhs (p : T) (A : set T) :
nbhs p A -> nbhs p (nbhs^~ A).
Proof. by move=> ?; rewrite {1}nbhs_principalE; apply/principal_filterP. Qed.

HB.instance Definition _ := @Nbhs_isNbhsTopological.Build T
Expand Down Expand Up @@ -101,16 +120,16 @@ Qed.
Local Lemma discrete_entourage_nbhsE : (@nbhs T _) = nbhs_ d.
Proof.
rewrite funeqE => x; rewrite nbhs_principalE eqEsubset; split => U.
move/principal_filterP => ?; exists diagonal; first by move=> ? [w _ <-].
move/principal_filterP => ?; exists diagonal; first by move=> ? [w _ <-].
by move=> z /= /set_mem; rewrite /diagonal /= => <-.
case => w entW wU; apply/principal_filterP; apply: wU; apply/mem_set.
exact: entW.
Qed.

HB.instance Definition _ := @Nbhs_isUniform.Build T
discrete_ent
discrete_entourage_filter
discrete_entourage_diagonal
discrete_ent
discrete_entourage_filter
discrete_entourage_diagonal
discrete_entourage_inv
discrete_entourage_split_ex
discrete_entourage_nbhsE.
Expand All @@ -119,12 +138,12 @@ HB.instance Definition _ := @Discrete_ofUniform.Build T erefl.

HB.end.

HB.factory Record DiscretePseudoMetric_ofUniform (R : numDomainType) T of
HB.factory Record DiscretePseudoMetric_ofUniform (R : numDomainType) T of
DiscreteUniform T := {}.

HB.builders Context R T of DiscretePseudoMetric_ofUniform R T.

Local Lemma discrete_ball_center x (eps : R) : 0 < eps ->
Local Lemma discrete_ball_center x (eps : R) : 0 < eps ->
@discrete_ball R T x eps x.
Proof. by []. Qed.

Expand All @@ -143,9 +162,9 @@ move=> entP; exists 1 => //= z z12; apply: entP; exists z.1 => //.
by rewrite {2}z12 -surjective_pairing.
Qed.

HB.instance Definition _ :=
@Uniform_isPseudoMetric.Build R T (@discrete_ball R T)
discrete_ball_center discrete_ball_sym discrete_ball_triangle
HB.instance Definition _ :=
@Uniform_isPseudoMetric.Build R T (@discrete_ball R T)
discrete_ball_center discrete_ball_sym discrete_ball_triangle
discrete_entourageE.

Local Lemma discrete_ballE : @ball R T = @discrete_ball R T.
Expand All @@ -155,9 +174,8 @@ HB.instance Definition _ := @Discrete_ofPseudometric.Build R T discrete_ballE.

HB.end.

(** we introducing an alias attaching discrete structures for
topology, uniformity, and pseudometric *)
Definition discrete_topology (T : Type) : Type := T.

HB.instance Definition _ (T : choiceType) :=
Choice.copy (discrete_topology T) T.
HB.instance Definition _ (T : pointedType) :=
Expand All @@ -166,9 +184,9 @@ HB.instance Definition _ (T : choiceType) :=
hasNbhs.Build (discrete_topology T) principal_filter.
HB.instance Definition _ (T : choiceType) :=
Discrete_ofNbhs.Build (discrete_topology T) erefl.
HB.instance Definition _ (T : choiceType) :=
HB.instance Definition _ (T : choiceType) :=
DiscreteUniform_ofNbhs.Build (discrete_topology T).
HB.instance Definition _ {R : numDomainType} (T : choiceType) :=
HB.instance Definition _ {R : numDomainType} (T : choiceType) :=
@DiscretePseudoMetric_ofUniform.Build R (discrete_topology T).

Section discrete_topology.
Expand Down

0 comments on commit 2e448c5

Please sign in to comment.