More definitions, following Ciraulo's Phd Thesis "Constructive Satisfiability".

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index ca544b598d190874ba01f6c13fd49db946651883..50671aa41afa50e12f3c3ebfdc6e18e5424e21e5 100644 (file)
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -147,4 +147,70 @@ theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U 
     cases (H4 i); clear H4; cases H; clear H;
     apply (H2 w); clear H2;
     assumption]
-qed.
\ No newline at end of file
+qed.
+
+definition singleton ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A.a=b).
+
+notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
+
+interpretation "singleton" 'singl a = (singleton _ a).
+
+definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {b}.
+
+interpretation "covered by one" 'leq a b = (leq _ a b).
+
+theorem leq_refl: ∀A:axiom_set.∀a:A. a ≤ a.
+ intros;
+ apply refl;
+ normalize;
+ reflexivity.
+qed.
+
+theorem leq_trans: ∀A:axiom_set.∀a,b,c:A. a ≤ b → b ≤ c → a ≤ c.
+ intros;
+ unfold in H H1 ⊢ %;
+ apply (transitivity ???? H);
+ constructor 1;
+ intros;
+ normalize in H2;
+ rewrite < H2;
+ assumption.
+qed.
+
+definition uparrow ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A. a ≤ b).
+
+notation "↑a" with precedence 80 for @{ 'uparrow $a }.
+
+interpretation "uparrow" 'uparrow a = (uparrow _ a).
+
+definition overlaps ≝ λA:Type.λU,V:2 \sup A.∃a:A. a ∈ U ∧ a ∈ V.
+
+notation "hvbox(a break ≬ b)" non associative with precedence 45
+for @{ 'overlaps $a $b }.
+
+interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
+
+definition intersects ≝ λA:Type.λU,V:2 \sup A.mk_powerset ? (λa:A. a ∈ U ∧ a ∈ V).
+
+notation "hvbox(a break ∩ b)" non associative with precedence 55
+for @{ 'intersects $a $b }.
+
+interpretation "intersects" 'intersects U V = (intersects _ U V).
+
+definition downarrow ≝ λA:axiom_set.λU:2 \sup A.mk_powerset ? (λa:A. ↑a ≬ U).
+
+notation "↓a" with precedence 80 for @{ 'downarrow $a }.
+
+interpretation "downarrow" 'downarrow a = (downarrow _ a).
+
+definition fintersects ≝ λA:axiom_set.λU,V:2 \sup A.↓U ∩ ↓V.
+
+notation "hvbox(U break ↓ V)" non associative with precedence 80 for @{ 'fintersects $U $V }.
+
+interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
+
+record convergent_generated_topology : Type ≝
+ { AA:> axiom_set;
+   convergence: ∀a:AA.∀U,V:2 \sup AA. a ◃ U → a ◃ V → a ◃ U ↓ V
+ }.
+