include "o-basic_pairs_to_o-basic_topologies.ma".
lemma rOR_full :
- ∀rS,rT:rOBP.∀f:arrows2 ? (OR (F2 ??? rS)) (OR (F2 ??? rT)).
- exT22 ? (λg:arrows2 OBP (F1 ??? rS) (F1 ??? rT).
- map_arrows2 ? ? OR rS rT g = f).
- ∀S,T.∀f. exT22 ? (λg. map_arrows2 ? ? OR S T g = f).
-arrows2 OBP S T
-unary_morphism1_setoid1 (OR S) (OR T)
+ ∀s,t:rOBP.∀f:arrows2 OBTop (OR (ℱ_2 s)) (OR (ℱ_2 t)).
+ exT22 ? (λg:arrows2 rOBP s t.
+ map_arrows2 ?? OR ?? (ℳ_2 g) = f).
+intro; cases s (s_2 s_1 s_eq); clear s; cases s_eq; clear s_eq s_2;
+intro; cases t (t_2 t_1 t_eq); clear t; cases t_eq; clear t_eq t_2;
+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;
+ [ 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)));
+ [ whd in Hletin; simplify in Hletin; 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;
+ ]
+ ]
+
+STOP;
+
(* Todo: rename BTop → OBTop *)