helm/software/matita/contribs/formal_topology/bin/old/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 = (leq A B).
  26
  27 axiom leq_refl: ∀A. A ⊆ A.
  28 axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B.
  29 axiom leq_tran: ∀A,B,C. A ⊆ B → B ⊆ C → A ⊆ C.
  30
  31 axiom i: S → S.
  32
  33 axiom i_contrattivita: ∀A. i A ⊆ A.
  34 axiom i_idempotenza: ∀A. i (i A) = i A.
  35 axiom i_monotonia: ∀A,B. A ⊆ B → i A ⊆ i B.
  36
  37 axiom c: S → S.
  38
  39 axiom c_espansivita: ∀A. A ⊆ c A.
  40 axiom c_idempotenza: ∀A. c (c A) = c A.
  41 axiom c_monotonia: ∀A,B. A ⊆ B → c A ⊆ c B.
  42
  43 axiom m: S → S.
  44
  45 axiom m_antimonotonia: ∀A,B. A ⊆ B → m B ⊆ m A.
  46 axiom m_saturazione: ∀A. A ⊆ m (m A).
  47 axiom m_puntofisso: ∀A. m A = m (m (m A)).
  48
  49 lemma l1: ∀A,B. i A ⊆ B → i A ⊆ i B.
  50  intros; rewrite < i_idempotenza; apply (i_monotonia (i A) B H).
  51 qed.
  52 lemma l2: ∀A,B. A ⊆ c B → c A ⊆ c B.
  53  intros; rewrite < c_idempotenza in ⊢ (? ? %); apply (c_monotonia A (c B) H).
  54 qed.
  55
  56 axiom th1: ∀A. c (m A) ⊆ m (i A).
  57 axiom th2: ∀A. i (m A) ⊆ m (c A).
  58
  59 (************** start of generated part *********************)
  60