matita/contribs/formal_topology/formal_topology2.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 comp: S → S → S.
  21 coercion cic:/matita/formal_topology/comp.con 1.
  22
  23 axiom comp_assoc: ∀A,B,C:S. A (B C) = (A B) C.
  24
  25 axiom one: S.
  26
  27 notation "1" with precedence 89
  28 for @{ 'unit }.
  29
  30 interpretation "Unit" 'unit =
  31  cic:/matita/formal_topology/one.con.
  32
  33 axiom one_left: ∀A. 1 A = A.
  34 axiom one_right: ∀A:S. A 1 = A.
  35
  36 axiom eps: S.
  37 axiom eps_idempotent: eps = eps eps.
  38
  39 notation "hvbox(A break ⊆ B)" with precedence 59
  40 for @{ 'subseteq $A $B}.
  41
  42 interpretation "Subseteq" 'subseteq A B =
  43  (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ A
  44   (cic:/matita/formal_topology/comp.con
  45    cic:/matita/formal_topology/eps.con B)).
  46
  47 axiom leq_refl: ∀A. A ⊆ A.
  48 axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B.
  49 axiom leq_tran: ∀A,B,C. A ⊆ B → B ⊆ C → A ⊆ C.
  50
  51 axiom i: S.
  52
  53 axiom i_contrattivita: i ⊆ 1.
  54 axiom i_idempotenza: i i = i.
  55 axiom i_monotonia: ∀A,B. A ⊆ B → i A ⊆ i B.
  56
  57 axiom c: S.
  58
  59 axiom c_espansivita: 1 ⊆ c.
  60 axiom c_idempotenza: c c = c.
  61 axiom c_monotonia: ∀A,B. A ⊆ B → c A ⊆ c B.
  62
  63 axiom m: S.
  64
  65 axiom m_antimonotonia: ∀A,B. A ⊆ B → m B ⊆ m A.
  66 axiom m_saturazione: 1 ⊆ m m.
  67 axiom m_puntofisso: m = m (m m).
  68
  69 theorem th1: c m ⊆ m i. intros; auto. qed.
  70 theorem th2: ∀A. i (m A) ⊆ (m (c A)). intros; auto. qed.
  71 theorem th3: ∀A. i A ⊆ (m (c (m A))). intros; auto. qed.
  72 theorem th4: ∀A. c A ⊆ (m (i (m A))). intros; auto. qed.
  73
  74 theorem th5: ∀A. i (m A) = i (m (c A)). intros; auto. qed.
  75 theorem th6: ∀A. m (i A) = c (m (i A)). intros; auto. qed.
  76
  77 theorem th7: ∀A. i (m (i A)) = i (s (i A)).