(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/formal_topologyxxx2/".
+set "baseuri" "cic:/matita/formal_topology/".
include "logic/equality.ma".
axiom S: Type.
notation "hvbox(A break ⊆ B)" with precedence 59
for @{ 'subseteq $A $B}.
-interpretation "Subseteq" 'subseteq A B =
- (cic:/matita/formal_topologyxxx2/leq.con A B).
+interpretation "Subseteq" 'subseteq A B = (leq A B).
axiom leq_refl: ∀A. A ⊆ A.
axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B.
axiom m_saturazione: ∀A. A ⊆ m (m A).
axiom m_puntofisso: ∀A. m A = m (m (m A)).
-lemma l1: ∀A,B. i A ⊆ B → i A ⊆ i B. intros; rewrite < i_idempotenza; auto. qed.
-lemma l2: ∀A,B. A ⊆ c B → c A ⊆ c B. intros; rewrite < c_idempotenza in ⊢ (? ? %); auto. qed.
+lemma l1: ∀A,B. i A ⊆ B → i A ⊆ i B.
+ intros; rewrite < i_idempotenza; apply (i_monotonia (i A) B H).
+qed.
+lemma l2: ∀A,B. A ⊆ c B → c A ⊆ c B.
+ intros; rewrite < c_idempotenza in ⊢ (? ? %); apply (c_monotonia A (c B) H).
+qed.
axiom th1: ∀A. c (m A) ⊆ m (i A).
axiom th2: ∀A. i (m A) ⊆ m (c A).