X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Fbasic_topologies.ma;h=0177afb63e9cea4035b289b1d8024dce1e795c32;hb=fa5cd121c672589afc0ac8ddd5d184897a38c7c6;hp=7ebec5e3f4607e968feb097b083d8c10457c606a;hpb=13088dbb8e54833dfbe2d6c38b08d78fc36452a8;p=helm.git diff --git a/helm/software/matita/library/formal_topology/basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_topologies.ma index 7ebec5e3f..0177afb63 100644 --- a/helm/software/matita/library/formal_topology/basic_topologies.ma +++ b/helm/software/matita/library/formal_topology/basic_topologies.ma @@ -24,12 +24,10 @@ record basic_topology: Type1 ≝ compatibility: ∀U,V. (A U ≬ J V) =_1 (U ≬ J V) }. -definition foo : ∀o1,o2:REL.carr1 (o1 ⇒_\r1 o2) → carr2 (setoid2_of_setoid1 (o1 ⇒_\r1 o2)) ≝ λo1,o2,x.x. - record continuous_relation (S,T: basic_topology) : Type1 ≝ { cont_rel:> S ⇒_\r1 T; reduced: ∀U. U =_1 J ? U → image_coercion ?? cont_rel U =_1 J ? (image_coercion ?? cont_rel U); - saturated: ∀U. U =_1 A ? U → (foo ?? cont_rel)⎻* U = _1A ? ((foo ?? cont_rel)⎻* U) + saturated: ∀U. U =_1 A ? U → (cont_rel)⎻* U = _1A ? ((cont_rel)⎻* U) }. definition continuous_relation_setoid: basic_topology → basic_topology → setoid1. @@ -48,7 +46,7 @@ coercion continuos_relation_of_continuous_relation_setoid. axiom continuous_relation_eq': ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2. - a = a' → ∀X.(foo ?? a)⎻* (A o1 X) = (foo ?? a')⎻* (A o1 X). + a = a' → ∀X.a⎻* (A o1 X) = a'⎻* (A o1 X). (* intros; split; intro; unfold minus_star_image; simplify; intros; [ cut (ext ?? a a1 ⊆ A ? X); [2: intros 2; apply (H1 a2); cases f1; assumption;] @@ -65,35 +63,34 @@ axiom continuous_relation_eq': [ apply I | assumption ]] qed.*) -axiom continuous_relation_eq_inv': +lemma continuous_relation_eq_inv': ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2. - (∀X.(foo ?? a)⎻* (A o1 X) = (foo ?? a')⎻* (A o1 X)) → a=a'. -(* intros 6; + (∀X.a⎻* (A o1 X) = a'⎻* (A o1 X)) → a=a'. + intros 6; cut (∀a,a': continuous_relation_setoid o1 o2. - (∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X)) → + (∀X.a⎻* (A o1 X) = a'⎻* (A o1 X)) → ∀V:o2. A ? (ext ?? a' V) ⊆ A ? (ext ?? a V)); - [2: clear b H a' a; intros; + [2: clear b f a' a; intros; lapply depth=0 (λV.saturation_expansive ??? (extS ?? a V)); [2: apply A_is_saturation;|skip] (* fundamental adjunction here! to be taken out *) - cut (∀V:Ω \sup o2.V ⊆ minus_star_image ?? a (A ? (extS ?? a V))); + cut (∀V:Ω^o2.V ⊆ a⎻* (A ? (extS ?? a V))); [2: intro; intros 2; unfold minus_star_image; simplify; intros; apply (Hletin V1 x); whd; split; [ exact I | exists; [apply a1] split; assumption]] clear Hletin; - cut (∀V:Ω \sup o2.V ⊆ minus_star_image ?? a' (A ? (extS ?? a V))); - [2: intro; apply (. #‡(H ?)); apply Hcut] clear H Hcut; + cut (∀V:Ω^o2.V ⊆ a'⎻* (A ? (extS ?? a V))); + [2: intro; apply (. #‡(f ?)^-1); apply Hcut] clear f Hcut; (* second half of the fundamental adjunction here! to be taken out too *) - intro; lapply (Hcut1 (singleton ? V)); clear Hcut1; + intro; lapply (Hcut1 {(V)}); clear Hcut1; unfold minus_star_image in Hletin; unfold singleton in Hletin; simplify in Hletin; whd in Hletin; whd in Hletin:(?→?→%); simplify in Hletin; apply (if ?? (A_is_saturation ???)); intros 2 (x H); lapply (Hletin V ? x ?); - [ apply refl | cases H; assumption; ] + [ apply refl | unfold foo; apply H; ] change with (x ∈ A ? (ext ?? a V)); - apply (. #‡(†(extS_singleton ????))); + apply (. #‡(†(extS_singleton ????)^-1)); assumption;] - split; apply Hcut; [2: assumption | intro; apply sym1; apply H] + split; apply Hcut; [2: assumption | intro; apply sym1; apply f] qed. -*) definition continuous_relation_comp: ∀o1,o2,o3. @@ -113,11 +110,11 @@ apply (s ∘ r) apply (.= (image_comp ??????)^-1); apply refl1] | intros; - apply sym1; unfold foo; - apply (.= †(minus_star_image_comp ??????)); - apply (.= (saturated ?? s ((foo ?? r)⎻* U) ?)^-1); + apply sym1; + apply (.= †(minus_star_image_comp ??? s r ?)); + apply (.= (saturated ?? s ((r)⎻* U) ?)^-1); [ apply (.= (saturated ?????)); [ assumption | apply refl1 ] - | change in ⊢ (? ? ? % ?) with (((foo ?? s)⎻* ∘ (foo ?? r)⎻* ) U); + | change in ⊢ (? ? ? % ?) with ((s⎻* ∘ r⎻* ) U); apply (.= (minus_star_image_comp ??????)^-1); apply refl1]] qed. @@ -145,26 +142,25 @@ definition BTop: category1. | intros; simplify; intro x; simplify; lapply depth=0 (continuous_relation_eq' ???? e) as H'; lapply depth=0 (continuous_relation_eq' ???? e1) as H1'; - letin K ≝ (λX.H1' (minus_star_image ?? (foo ?? a) (A ? X))); clearbody K; + letin K ≝ (λX.H1' ((a)⎻* (A ? X))); clearbody K; cut (∀X:Ω \sup o1. - minus_star_image o2 o3 (foo ?? b) (A o2 (minus_star_image o1 o2 (foo ?? a) (A o1 X))) - =_1 minus_star_image o2 o3 (foo ?? b') (A o2 (minus_star_image o1 o2 (foo ?? a') (A o1 X)))); + (b)⎻* (A o2 ((a)⎻* (A o1 X))) + =_1 (b')⎻* (A o2 ((a')⎻* (A o1 X)))); [2: intro; apply sym1; apply (.= (†(†((H' X)^-1)))); apply sym1; apply (K X);] clear K H' H1'; -alias symbol "compose" (instance 1) = "category1 composition". -alias symbol "compose" (instance 1) = "category1 composition". -alias symbol "compose" (instance 1) = "category1 composition". +alias symbol "powerset" (instance 5) = "powerset low". +alias symbol "compose" (instance 2) = "category1 composition". cut (∀X:Ω^o1. - minus_star_image ?? (foo ?? (b ∘ a)) (A o1 X) =_1 minus_star_image ?? (foo ?? (b'∘a')) (A o1 X)); + ((b ∘ a))⎻* (A o1 X) =_1 ((b'∘a'))⎻* (A o1 X)); [2: intro; unfold foo; apply (.= (minus_star_image_comp ??????)); - change in ⊢ (? ? ? % ?) with ((foo ?? b)⎻* ((foo ?? a)⎻* (A o1 X))); + change in ⊢ (? ? ? % ?) with ((b)⎻* ((a)⎻* (A o1 X))); apply (.= †(saturated ?????)); [ apply ((saturation_idempotent ????)^-1); apply A_is_saturation ] apply sym1; apply (.= (minus_star_image_comp ??????)); - change in ⊢ (? ? ? % ?) with ((foo ?? b')⎻* ((foo ?? a')⎻* (A o1 X))); + change in ⊢ (? ? ? % ?) with ((b')⎻* ((a')⎻* (A o1 X))); apply (.= †(saturated ?????)); [ apply ((saturation_idempotent ????)^-1); apply A_is_saturation ] apply ((Hcut X)^-1)]