1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/formal_topology/".
16 include "logic/equality.ma".
20 axiom leq: S → S → Prop.
22 notation "hvbox(A break ⊆ B)" with precedence 59
23 for @{ 'subseteq $A $B}.
25 interpretation "Subseteq" 'subseteq A B =
26 (cic:/matita/formal_topology/leq.con A B).
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.
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.
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.
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)).
50 lemma l1: ∀A,B. i A ⊆ B → i A ⊆ i B.
51 intros; rewrite < i_idempotenza; apply (i_monotonia (i A) B H).
53 lemma l2: ∀A,B. A ⊆ c B → c A ⊆ c B.
54 intros; rewrite < c_idempotenza in ⊢ (? ? %); apply (c_monotonia A (c B) H).
57 axiom th1: ∀A. c (m A) ⊆ m (i A).
58 axiom th2: ∀A. i (m A) ⊆ m (c A).
60 (************** start of generated part *********************)