2 files changed, 8 insertions(+), 8 deletions(-)
R Miscellaneous.v => Dynamical.v
M _CoqProject
R Miscellaneous.v => Dynamical.v +7 -7
@@ 1,5 1,7 @@
-(* Miscellaneous properties *)
+(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
+ * Miscellaneous properties regarding discrete-time dynamical systems
+ * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)
Section Power.
@@ 14,13 16,11 @@ Section Power.
End Power.
-Require Topology.Continuity.
+Require Import Topology.Continuity.
Section Discrete_Time.
- (* Discrete-Time Autonomous Dynamical System *)
-
- Import Topology.Continuity.
+ (* Discrete-time autonomous topological dynamical system *)
Variable X: TopologicalSpace.
@@ 34,7 34,7 @@ Section Discrete_Time.
- apply (continuous_composition F); trivial.
Qed.
- Section Local.
+ Section Local_Properties.
Variable x: point_set X.
@@ 56,7 56,7 @@ Section Discrete_Time.
exists n; assumption.
Qed.
- End Local.
+ End Local_Properties.
Definition perfect := forall x: point_set X, ~ isolated x.
M _CoqProject => _CoqProject +1 -1
@@ 15,6 15,6 @@ Languages.v
Patterns_US.v
Local_Rule.v
Prodiscrete.v
-Miscellaneous.v
+Dynamical.v
Metric_Space.v
Decidable.v