Module mathcomp.analysis.topology_theory.discrete_topology

From HB Require Import structures.
From mathcomp Require Import boot order algebra all_classical all_reals.
From mathcomp Require Import topology_structure uniform_structure.
From mathcomp Require Import order_topology pseudometric_structure compact.

# 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 == an order type with the discrete topology pdiscreteTopologicalType == pointed type with the discrete topology pdiscreteOrderTopologicalType == pointed, ordered, and discrete discreteUniformType == a uniform space where the diagonal is an entourage discretePseudoMetricType == a pseudometric space where the only balls are singletons discrete_topology T == alias attaching discrete structures for topology, uniformity, and pseudometric ```

Unset SsrOldRewriteGoalsOrder.

Import Order.TTheory GRing.Theory Num.Def Num.Theory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

. T := {
nbhs_principalE : (@nbhs T _) = principal_filter;
}.

()
. of Nbhs T & Discrete_ofNbhs T}.

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

Note: having the discrete topology does not guarantee the discrete uniformity. Likewise for the discrete metric. Consider set 1/n | n in R

. T := {
  uniform_discrete : @entourage T = discrete_ent
}.

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

. T &
    PseudoMetric R T := {
  metric_discrete : @ball R T = @discrete_ball R T
}.

()
.
  { of DiscreteNbhs T & Topological T}.

()
.
  { of Discrete_ofNbhs T & OrderTopological d T}.

()
.
  { of DiscreteTopology T & Pointed T}.

()
.
  { of Discrete_ofNbhs T & OrderTopological d T & Pointed T}.

()
.
  { of Discrete_ofUniform T & Uniform T & Discrete_ofNbhs T}.

()
. :=
  { of Discrete_ofPseudometric R T & PseudoMetric R T & DiscreteUniform T}.

. T.

Local Lemma ( : T) : ProperFilter (nbhs p).

Proof.

rewrite nbhs_principalE; exact: principal_filter_proper. Qed.

Local Lemma ( : T) ( : set T) : nbhs p A -> A p.

Proof.

by rewrite nbhs_principalE => /principal_filterP. Qed.

Local Lemma ( : T) ( : set T) :
nbhs p A -> nbhs p (nbhs^~ A).

Proof.

by move=> ?; rewrite {1}nbhs_principalE; apply/principal_filterP. Qed.

..Build T
principal_nbhs_filter principal_nbhs_singleton principal_nbhs_nbhs.

..

. T & Nbhs T := {}.
. T.

Local Open Scope relation_scope.

Local Notation := (@discrete_ent T).

Local Lemma : Filter d.

Proof.

exact: globally_filter. Qed.

Local Lemma : forall , d A -> diagonal `<=` A.

Proof.

by move=> ? + x x12; apply; exists x.1; rewrite // {2}x12 -surjective_pairing.
Qed.

Local Lemma : forall , d A -> d A^-1.

Proof.

by move=> ? dA x [i _ <-]; apply: dA; exists i. Qed.

Local Lemma :
forall , d A -> exists2 , d B & B \; B `<=` A.

Proof.

move=> ? dA; exists (range (fun => (x, x))) => //.
by rewrite set_compose_diag => x [i _ <-]; apply: dA; exists i.
Qed.

Local Lemma : (@nbhs T _) = nbhs_ d.

Proof.

rewrite funeqE => x; rewrite nbhs_principalE eqEsubset; split => U.
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.

..Build T
  discrete_ent
  discrete_entourage_filter
  discrete_entourage_diagonal
  discrete_entourage_inv
  discrete_entourage_split_ex
  discrete_entourage_nbhsE.

..Build T erefl.

..

. () T &
  DiscreteUniform T := {}.

. R T.

Local Lemma ( : R) : 0 < eps ->
  @discrete_ball R T x eps x.

Proof.

by []. Qed.

Local Lemma ( : T) ( : R) :
discrete_ball x e y -> discrete_ball y e x.

Proof.

by move=>->. Qed.

Local Lemma ( :T) ( : R) :
discrete_ball x e1 y -> discrete_ball y e2 z -> discrete_ball x (e1 + e2) z.

Proof.

by move=> -> ->. Qed.

Local Lemma : entourage = entourage_ (@discrete_ball R T).

Proof.

rewrite predeqE => P; rewrite uniform_discrete; split; last first.
by move=> dbP ? [?] _ <-; move: dbP; case => /= ? ?; apply.
move=> entP; exists 1 => //= z z12; apply: entP; exists z.1 => //.
by rewrite {2}z12 -surjective_pairing.
Qed.

.
  .Build R T (@discrete_ball R T)
    discrete_ball_center discrete_ball_sym discrete_ball_triangle
    discrete_entourageE.

Local Lemma : @ball R T = @discrete_ball R T.

Proof.

by rewrite funeq2E => ? ?. Qed.

..Build R T discrete_ballE.

..

Definition ( : Type) : Type := T.

. () :=
  Choice.copy (discrete_topology T) T.
. () :=
  Pointed.on (discrete_topology T).
. () :=
  hasNbhs.Build (discrete_topology T) principal_filter.
. () :=
  Discrete_ofNbhs.Build (discrete_topology T) erefl.
..
. () :=
  DiscreteUniform_ofNbhs.Build (discrete_topology T).
. (T : choiceType) :=
  @DiscretePseudoMetric_ofUniform.Build R (discrete_topology T).

Section discrete_topology.

Context { : discreteTopologicalType}.

Lemma ( : set X) : open A.

Proof.

rewrite openE => ? ?; rewrite /interior nbhs_principalE.
exact/principal_filterP.
Qed.

Lemma ( : X) : nbhs x [set x].

Proof.

by apply: open_nbhs_nbhs; split => //; exact: discrete_open. Qed.

Lemma ( : set X) : closed A.

Proof.

by rewrite -[A]setCK closedC; exact: discrete_open. Qed.

Lemma ( : set_system X) ( : X) :
Filter F -> F --> x <-> F [set x].

Proof.

rewrite nbhs_principalE nbhs_simpl; split; first by exact.
by move=> Fx U /principal_filterP ?; apply: filterS Fx => ? ->.
Qed.

End discrete_topology.

Files

Module mathcomp.analysis.topology_theory.discrete_topology