include "o-basic_pairs_to_o-basic_topologies.ma".
+lemma category2_of_category1_respects_comp_r:
+ ∀C:category1.∀o1,o2,o3:C.
+ ∀f:arrows1 ? o1 o2.∀g:arrows1 ? o2 o3.
+ (comp1 ???? f g) =_\ID (comp2 (category2_of_category1 C) o1 o2 o3 f g).
+ intros; constructor 1;
+qed.
+
+lemma category2_of_category1_respects_comp:
+ ∀C:category1.∀o1,o2,o3:C.
+ ∀f:arrows1 ? o1 o2.∀g:arrows1 ? o2 o3.
+ (comp2 (category2_of_category1 C) o1 o2 o3 f g) =_\ID (comp1 ???? f g).
+ intros; constructor 1;
+qed.
+
+lemma POW_full':
+ ∀S,T:REL.∀f:arrows2 SET1 (POW S) (POW T).
+ arrows1 REL S T.
+ intros;
+ constructor 1; constructor 1;
+ [ intros (x y); apply (y ∈ c {(x)});
+ | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
+ apply (e1ࠠe); ]
+qed.
+
+(*
+lemma POW_full_image:
+ ∀S,T:REL.∀f:arrows2 SET1 (POW S) (POW T).
+ exT22 ? (λg:arrows1 REL S T.or_f ?? (map_arrows2 ?? POW S T g) = f).
+ intros; letin g ≝ (? : carr1 (arrows1 REL S T)); [
+ constructor 1; constructor 1;
+ [ intros (x y); apply (y ∈ f {(x)});
+ | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
+ apply (e1ࠠe); ]]
+exists [apply g]
+intro; split; intro; simplify; intro;
+[ whd in f1; change in f1:(? ? (λ_:?.? ? ? ? ? % ?)) with (a1 ∈ f {(x)});
+ cases f1; cases x; clear f1 x; change with (a1 ∈ f a);
+ lapply (f_image_monotone ?? (map_arrows2 ?? POW S T g) (singleton ? w) a ? a1);
+ [2: whd in Hletin;
+ change in Hletin:(? ? (λ_:?.? ? ? ? ? % ?))
+ with (a1 ∈ f {(x)}); cases Hletin; cases x;
+ [ intros 2; change in f3 with (eq1 ? w a2); change with (a2 ∈ a);
+ apply (. f3^-1‡#); assumption;
+ | assumption; ]
+
+
+
+ lapply (. (or_prop3 ?? (map_arrows2 ?? POW S T g) (singleton ? a1) a)^-1);
+ [ whd in Hletin:(? ? ? ? ? ? %);
+ change in Hletin:(? ? ? ? ? ? (? ? (? ? ? (λ_:?.? ? (λ_:?.? ? ? ? ? % ?)) ?)))
+ with (y ∈ f {(x)});
+ cases Hletin; cases x1; cases x2;
+
+ [ cases Hletin; change in x with (eq1 ? a1 w1); apply (. x‡#); assumption;
+ | exists; [apply w] assumption ]
+
+
+ clear g;
+ cases f1; cases x; simplify in f2; change with (a1 ∈ (f a));
+ lapply depth=0 (let x ≝ POW in or_prop3 (POW S) (POW T) (map_arrows2 ?? POW S T g));
+ lapply (Hletin {(w)} {(a1)}).
+ lapply (if ?? Hletin1); [2: clear Hletin Hletin1;
+ exists; [apply a1] [whd; exists[apply w] split; [assumption;|change with (w = w); apply rule #]]
+ change with (a1=a1); apply rule #;]
+ clear Hletin Hletin1; cases Hletin2; whd in x2;
+qed.
+*)
+lemma curry: ∀A,B,C.binary_morphism1 A B C → A → B ⇒ C.
+ intros;
+ constructor 1;
+ [ apply (b c);
+ | intros; apply (#‡e); ]
+qed.
+
+notation < "F x" left associative with precedence 60 for @{'map_arrows $F $x}.
+interpretation "map arrows 2" 'map_arrows F x = (fun12 _ _ (map_arrows2 _ _ F _ _) x).
+
+definition preserve_sup : ∀S,T.∀ f:Ω \sup S ⇒ Ω \sup T. CProp1.
+intros (S T f); apply (∀X:Ω \sup S. (f X) = ?);
+constructor 1; constructor 1;
+[ intro y; alias symbol "singl" = "singleton". alias symbol "and" = "and_morphism".
+ apply (∃x:S. x ∈ X ∧ y ∈ f {(x)});
+| intros (a b H); split; intro E; cases E; clear E; exists; [1,3:apply w]
+ [ apply (. #‡(H^-1‡#)); | apply (. #‡(H‡#));] assumption]
+qed.
+
+alias symbol "singl" = "singleton".
+lemma eq_cones_to_eq_rel:
+ ∀S,T. ∀f,g: arrows1 REL S T.
+ (∀x. curry ??? (image ??) f {(x)} = curry ??? (image ??) g {(x)}) → f = g.
+intros; intros 2 (a b); split; intro;
+[ cases (f1 a); lapply depth=0 (s b); clear s s1;
+ lapply (Hletin); clear Hletin;
+ [ cases Hletin1; cases x; change in f4 with (a = w);
+ change with (a ♮g b); apply (. f4‡#); assumption;
+ | exists; [apply a] split; [ assumption | change with (a=a); apply rule #;]]
+| cases (f1 a); lapply depth=0 (s1 b); clear s s1;
+ lapply (Hletin); clear Hletin;
+ [ cases Hletin1; cases x; change in f4 with (a = w);
+ change with (a ♮f b); apply (. f4‡#); assumption;
+ | exists; [apply a] split; [ assumption | change with (a=a); apply rule #;]]]
+qed.
+
+variant eq_cones_to_eq_rel':
+ ∀S,T. ∀f,g: arrows1 REL S T.
+ (∀x:S. or_f ?? (map_arrows2 ?? POW S T f) {(x)} = or_f ?? (map_arrows2 ?? POW S T g) {(x)}) →
+ f = g
+≝ eq_cones_to_eq_rel.
+
lemma rOR_full :
∀s,t:rOBP.∀f:arrows2 OBTop (OR (ℱ_2 s)) (OR (ℱ_2 t)).
exT22 ? (λg:arrows2 rOBP s t.
cases t_eq; clear t_eq t_2;
letin t1 ≝ (BP_to_OBP t_1); change in match (BP_to_OBP t_1) with t1;
whd in ⊢ (%→?); whd in ⊢ (? (? ? ? ? %) (? ? ? ? %)→?);
-intro; whd in s_1 t_1;
-letin R ≝ (? : (carr2 (arrows2 (category2_of_category1 BP) s_1 t_1)));
- [2:
- exists;
+intro; whd in s_1 t_1;
+letin R ≝ (? : (carr2 (arrows2 (category2_of_category1 BP) s_1 t_1)));
+[2:
+ exists;
[ constructor 1;
[2: simplify; apply R;
| simplify; apply (fun12 ?? (map_arrows2 ?? BP_to_OBP s_1 t_1)); apply R;
| simplify; apply rule #; ]]
simplify;
- | constructor 1;
- [2: constructor 1; constructor 1;
- [ intros (x y); apply (y ∈ f (singleton ? x));
- | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
- unfold in ⊢ (? ? ? (? ? ? ? ? ? %) ?); apply (.= e1‡††e);
- apply rule #; ]
- |1: constructor 1; constructor 1;
- [ intros (x y); apply (y ∈ star_image ?? (⊩ \sub t_1) (f (image ?? (⊩ \sub s_1) (singleton ? x))));
- | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation;
- unfold in ⊢ (? ? ? (? ? ? ? ? ? (? ? ? ? ? ? %)) ?);
- apply (.= e1‡(#‡†(#‡†e))); apply rule #; ]
- | whd; simplify; intros; simplify;
- whd in ⊢ (? % %); simplify in ⊢ (? % %);
- lapply (Oreduced ?? f (image (concr s_1) (form s_1) (⊩ \sub s_1) (singleton ? x)));
- [ cases Hletin; clear Hletin;
- lapply (s y); clear s;
-whd in Hletin:(? ? ? (? ? (? ? ? % ?)) ?); simplify in Hletin;
-whd in Hletin; simplify in Hletin;
- lapply (s1 y); clear s1;
- split; intros; simplify; whd in f1 ⊢ %; simplify in f1 ⊢ %;
- cases f1; clear f1; cases x1; clear x1;
- [
- | exists;
- ]
+|1: constructor 1;
+ [2: apply (pi1exT22 ?? (POW_full (form s_1) (form t_1) f));
+ |1: letin u ≝ (or_f_star ?? (map_arrows2 ?? POW (concr t_1) (form t_1) (⊩ \sub t_1)));
+ letin r ≝ (u ∘ (or_f ?? f));
+ letin xxx ≝ (or_f ?? (map_arrows2 ?? POW (concr s_1) (form s_1) (⊩ \sub s_1)));
+ letin r' ≝ (r ∘ xxx); clearbody r';
+ apply (POW_full' (concr s_1) (concr t_1) r');
+ | simplify in ⊢ (? ? ? (? ? ? ? ? % ?) ?);
+ apply eq_cones_to_eq_rel'; intro;
+ apply
+ (cic:/matita/logic/equality/eq_elim_r''.con ?????
+ (category2_of_category1_respects_comp_r : ?));
+ apply rule (.= (#‡#));
+ apply (.= (respects_comp2 ?? POW (concr s_1) (concr t_1) (form t_1) ? (⊩\sub t_1))‡#);
+ apply sym2;
+ apply (.= (respects_comp2 ?? POW (concr s_1) (form s_1) (form t_1) (⊩\sub s_1) (pi1exT22 ?? (POW_full (form s_1) (form t_1) (Ocont_rel ?? f)))));
+ apply (let H ≝(\snd (POW_full (form s_1) (form t_1) (Ocont_rel ?? f))) in .= #‡H);
+ apply sym2;
]
STOP;
projects / helm.git / commitdiff