]> matita.cs.unibo.it Git - helm.git/blob - matita/contribs/formal_topology/formal_topology.ma
natural number => Coq natural number
[helm.git] / matita / contribs / formal_topology / formal_topology.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/formal_topology/".
16 include "logic/equality.ma".
17
18 axiom S: Type.
19
20 axiom leq: S → S → Prop.
21
22 notation "hvbox(A break ⊆ B)" with precedence 59
23 for @{ 'subseteq $A $B}.
24
25 interpretation "Subseteq" 'subseteq A B =
26  (cic:/matita/formal_topology/leq.con A B).
27
28 axiom leq_refl: ∀A. A ⊆ A.
29 axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B.
30 axiom leq_tran: ∀A,B,C. A ⊆ B → B ⊆ C → A ⊆ C.
31
32 axiom i: S → S.
33
34 axiom i_contrattivita: ∀A. i A ⊆ A.
35 axiom i_idempotenza: ∀A. i (i A) = i A.
36 axiom i_monotonia: ∀A,B. A ⊆ B → i A ⊆ i B.
37
38 axiom c: S → S.
39
40 axiom c_espansivita: ∀A. A ⊆ c A.
41 axiom c_idempotenza: ∀A. c (c A) = c A.
42 axiom c_monotonia: ∀A,B. A ⊆ B → c A ⊆ c B.
43
44 axiom m: S → S.
45
46 axiom m_antimonotonia: ∀A,B. A ⊆ B → m B ⊆ m A.
47 axiom m_saturazione: ∀A. A ⊆ m (m A).
48 axiom m_puntofisso: ∀A. m A = m (m (m A)).
49
50 lemma l1: ∀A,B. i A ⊆ B → i A ⊆ i B. intros; rewrite < i_idempotenza; auto. qed.
51 lemma l2: ∀A,B. A ⊆ c B → c A ⊆ c B. intros; rewrite < c_idempotenza in ⊢ (? ? %); auto. qed.
52
53 theorem geq1: ∀A. i (i A) = i A. intros. auto. qed.
54 theorem geq2: ∀A. c (c A) = c A. intros. auto. qed.
55 theorem geq3: ∀A. i (i (c A)) = i (c A). intros. auto. qed.
56 theorem geq4: ∀A. c (c (i A)) = c (i A). intros. auto. qed.
57 theorem geq5: ∀A. i (c (i (c A))) = i (c A). intros. auto depth=4. qed.
58 theorem geq6: ∀A. c (i (c (i A))) = c (i A). intros. auto depth=4. qed.
59 theorem gse1: ∀A. i A ⊆ A. intros. auto. qed.
60 theorem gse2: ∀A. A ⊆ c A. intros. auto. qed.
61 theorem gse3: ∀A. i A ⊆ i (c (i A)). intros. auto. qed.
62 theorem gse4: ∀A. i (c (i A)) ⊆ i (c A). intros. auto. qed.
63 theorem gse5: ∀A. i (c (i A)) ⊆ c (i A). intros. auto. qed.
64 theorem gse6: ∀A. i (c A) ⊆ c (i (c A)). intros. auto. qed.
65 theorem gse7: ∀A. c (i A) ⊆ c (i (c A)). intros. auto. qed.
66 theorem gse8: ∀A. c (i (c A)) ⊆ c A. intros. auto. qed.
67
68 axiom th1: ∀A. c (m A) ⊆ m (i A).
69 axiom th2: ∀A. i (m A) ⊆ m (c A).
70
71 theorem se1: ∀A. i (c (m (c A))) ⊆ i (m (i (c A))). intros; auto. qed.
72 theorem se2: ∀A. i (m (i (c A))) ⊆ m (c (i (c A))). intros; auto. qed.
73 theorem se3: ∀A. c (i (m A)) ⊆ c (i (c (m (c A)))). intros; auto depth=4. qed.
74 theorem se4: ∀A. c (i (c (m (c A)))) ⊆ c (i (m (i (c A)))). intros; auto. qed.
75 theorem se5: ∀A. i (c (m (c A))) ⊆ c (i (c (m (c A)))). intros; auto. qed.
76 theorem se6: ∀A. i (m (i (c A))) ⊆ c (i (m (i (c A)))). intros; auto. qed.
77 theorem se7: ∀A. m (c A) ⊆ m A. intros; auto. qed.
78 theorem se8: ∀A. i (c (m (c A))) ⊆ i (c (m A)). intros; auto. qed.
79 theorem se9: ∀A. i (c (m A)) ⊆ i (m (i A)). intros; auto. qed.
80 theorem se10: ∀A. i (m (i (c A))) ⊆ i (m (i A)). intros; auto depth=4. qed.
81 theorem se11: ∀A. i (m (i A)) ⊆ m (c (i A)). intros; auto. qed.
82 theorem se12: ∀A. m (c (i (c A))) ⊆ m (c (i A)). intros; auto. qed.
83 theorem se13: ∀A. m (c A) ⊆ m (c (i (c A))). intros; auto. qed.
84 theorem se14: ∀A. i (c (m A)) ⊆ c (i (c (m A))). intros; auto. qed.
85 theorem se15: ∀A. c (i (c (m A))) ⊆ c (m A). intros; auto. qed.
86 theorem se16: ∀A. c (i (m (i A))) ⊆ c (m (c (i A))). intros; auto depth=4. qed.
87 theorem se17: ∀A. c (m (c (i A))) ⊆ m (i (c (i A))). intros; auto. qed.
88 theorem se18: ∀A. m (i (c A)) ⊆ m (i (c (i A))). intros; auto. qed.
89 theorem se19: ∀A. m (i (c (i A))) ⊆ m (i A). intros; auto. qed.
90 theorem se20: ∀A. c (m (c A)) ⊆ c (m A). intros; auto. qed.
91 theorem se21: ∀A. c (m (c A)) ⊆ c (m (c (i (c A)))). intros; auto. qed.
92 theorem se22: ∀A. c (m (c (i (c A)))) ⊆ m (i (c A)). intros; auto. qed.
93 theorem se23: ∀A. c (i (c (m (c A)))) ⊆ c (i (c (m A))). intros; auto. qed.
94 theorem se24: ∀A. c (i (c (m (c A)))) ⊆ c (m (c A)). intros; auto. qed.
95 theorem se25: ∀A. m (c A) ⊆ c (m (c A)). intros; auto. qed.
96 theorem se26: ∀A. c (i (m (i (c A)))) ⊆ c (i (m (c (i (c A))))). intros; auto. qed.
97 theorem se27: ∀A. m (c (i (c A))) ⊆ c (m (c (i (c A)))). intros; auto. qed.
98 theorem se28: ∀A. m (c (i A)) ⊆ c (m (c (i A))). intros; auto. qed.
99 theorem se29: ∀A. m A ⊆ c (m A). intros; auto. qed.
100 theorem se30: ∀A. i (m A) ⊆ i (c (i (m A))). intros; auto. qed.
101 theorem se31: ∀A. i (c (i (m A))) ⊆ c (i (m A)). intros; auto. qed.
102 theorem se32: ∀A. i (c (i (m A))) ⊆ i (c (m (c A))). intros; auto. qed.
103 theorem se33: ∀A. c (i (c (m A))) ⊆ c (i (m (i A))). intros; auto. qed.
104 theorem se34: ∀A. i (m (i A)) ⊆ c (i (m (i A))). intros; auto. qed.
105 theorem se35: ∀A. c (i (m (i (c A)))) ⊆ c (i (m (i A))). intros; auto. qed.
106 theorem se36: ∀A. c (m (c (i (c A)))) ⊆ c (m (c (i A))). intros; auto. qed.
107
108 theorem th5: ∀A. i (m (c A)) = i (m A). intros; auto depth=4. qed.
109 theorem th6: ∀A. c (m (i A)) = m (i A). intros; auto width=2 depth=5. qed.
110 theorem th7: ∀A. i (m (i A)) = i (c (i (m (i A)))). intros; auto. qed.
111 theorem th8: ∀A. i (m (i A)) = i (m (i (c (i A)))). intros; auto. qed.
112 theorem th9: ∀A. i (c (m (c (i A)))) = i (m (i A)). intros; auto depth=4. qed.
113
114 (* theorem th7: ∀A. i (m (i A)) = i (s (i A)). *)