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.
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;]
[ 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.
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.
| 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)]
| cases daemon (*apply o_relation_topology_of_relation_topology_morphism_respects_comp*);]
qed.
-(* FIXME
-alias symbol "eq" (instance 2) = "setoid1 eq".
-alias symbol "eq" (instance 1) = "setoid2 eq".
theorem BTop_to_OBTop_faithful: faithful2 ?? BTop_to_OBTop.
- intros 5;
- whd in e; unfold BTop_to_OBTop in e; simplify in e;
- change in match (oA ?) in e with (A o1);
- whd in f g;
- alias symbol "OR_f_minus_star" (instance 1) = "relation f⎻*".
- change in match ((o_continuous_relation_of_continuous_relation_morphism o1 o2 f)⎻* ) in e with ((foo ?? f)⎻* );
- change in match ((o_continuous_relation_of_continuous_relation_morphism o1 o2 g)⎻* ) in e with ((foo ?? g)⎻* );
- whd; whd in o1 o2;
- intro b;
- alias symbol "OR_f_minus" (instance 1) = "relation f⎻".
- letin fb ≝ ((ext ?? f) b);
- lapply (e fb);
- whd in Hletin:(? ? ? % %);
- cases (Hletin); simplify in s s1;
- split;
- [2: intro; simplify;
- lapply depth=0 (s b); intro; apply (Hletin1 ? a ?)
- [ 2: whd in f1;
- change in Hletin with ((foo ?? f)⎻*
-
- alias symbol "OR_f_minus_star" (instance 4) = "relation f⎻*".
- alias symbol "OR_f_minus_star" (instance 4) = "relation f⎻*".
-change in e with
- (comp2 SET1 (Ω^o1) (Ω^o1) (Ω^o2) (A o1) (foo o1 o2 f)⎻* =_1
- comp2 SET1 (Ω^o1) (Ω^o1) (Ω^o2) (A o1) (foo o1 o2 g)⎻*
- );
-
-
-
- change in e with (comp1 SET (Ω^o1) ?? (A o1) (foo o1 o2 f)⎻* = ((foo o1 o2 g)⎻* ∘ A o1));
- unfold o_continuous_relation_of_continuous_relation_morphism in e;
- unfold o_continuous_relation_of_continuous_relation in e;
- simplify in e;
+ intros 5; apply (continuous_relation_eq_inv' o1 o2 f g); apply e;
qed.
include "formal_topology/notation.ma".
-theorem BTop_to_OBTop_full:
- ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? BTop_to_OBTop S T g = f).
- intros;
+theorem BTop_to_OBTop_full: full2 ?? BTop_to_OBTop.
+ intros 3 (S T);
cases (POW_full (carrbt S) (carrbt T) (Ocont_rel ?? f)) (g Hg);
- exists[
+ (* cases Hg; *)
+ exists [
constructor 1;
[ apply g
- | apply hide; intros; lapply (Oreduced ?? f ? e);
+ | unfold image_coercion; cases daemon (*apply hide; intros; lapply (Oreduced ?? f ? e); unfold image_coercion;
cases Hg; lapply (e3 U) as K; apply (.= K);
- apply (.= Hletin); apply rule (†(K^-1));
- | apply hide; intros; lapply (Osaturated ?? f ? e);
+ apply (.= Hletin); apply rule (†(K^-1)); *)
+ | cases daemon (* apply hide; intros; lapply (Osaturated ?? f ? e);
cases Hg; lapply (e1 U) as K; apply (.= K);
- apply (.= Hletin); apply rule (†(K^-1));
+ apply (.= Hletin); apply rule (†(K^-1)); *)
]
| simplify; unfold BTop_to_OBTop; simplify;
+ cases Hg; unfold o_continuous_relation_of_continuous_relation_morphism;
+ simplify;
+ change with ((orelation_of_relation ?? g)⎻* ∘ oA (o_basic_topology_of_basic_topology S) =
+ f⎻* ∘ oA (o_basic_topology_of_basic_topology S));
+
+
+ change with (g⎻* ∘ oA (o_basic_topology_of_basic_topology S) =
+ f⎻* ∘ oA (o_basic_topology_of_basic_topology S));
+ apply sym2; whd in T;
+ intro;
+ apply trans2; [2: apply sym2; [2: apply Hg;
+
+ whd in ⊢ (?(??%%)???);
+ apply (.= Hg^-1);
unfold o_continuous_relation_of_continuous_relation_morphism; simplify;
- cases Hg; whd; simplify; intro;
+ intro; simplify;
+ unfold image_coercion; cases Hg; whd; simplify; intro; simplify;
qed.
*)
apply (. (#‡e1)); whd in e; apply (fi ?? (e ??));assumption]]
qed.
-(*
-definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
+definition extS: ∀X,S:REL. ∀r:X ⇒_\r1 S. Ω^S ⇒_1 Ω^X.
(* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*)
intros (X S r); constructor 1;
[ intro F; constructor 1; constructor 1;
[ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a);
| intros; split; intro; cases f (H1 H2); clear f; split;
- [ apply (. (H‡#)); assumption
- |3: apply (. (H\sup -1‡#)); assumption
+ [ apply (. (e^-1‡#)); assumption
+ |3: apply (. (e‡#)); assumption
|2,4: cases H2 (w H3); exists; [1,3: apply w]
- [ apply (. (#‡(H‡#))); assumption
- | apply (. (#‡(H \sup -1‡#))); assumption]]]
- | intros; split; simplify; intros; cases f; cases H1; split;
+ [ apply (. (#‡(e^-1‡#))); assumption
+ | apply (. (#‡(e‡#))); assumption]]]
+ | intros; split; simplify; intros; cases f; cases e1; split;
[1,3: assumption
|2,4: exists; [1,3: apply w]
- [ apply (. (#‡H)‡#); assumption
- | apply (. (#‡H\sup -1)‡#); assumption]]]
+ [ apply (. (#‡e^-1)‡#); assumption
+ | apply (. (#‡e)‡#); assumption]]]
qed.
-
+(*
lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id1 ? o) X = X.
intros;
unfold extS; simplify;
[ apply (. e^-1 a2 w); | apply (. e a2 w)] assumption;]
qed.
-interpretation "relation f⎻*" 'OR_f_minus_star r = (fun12 ?? (minus_star_image ? ?) r).
-interpretation "relation f⎻" 'OR_f_minus r = (fun12 ?? (minus_image ? ?) r).
-interpretation "relation f*" 'OR_f_star r = (fun12 ?? (star_image ? ?) r).
+definition foo : ∀o1,o2:REL.carr1 (o1 ⇒_\r1 o2) → carr2 (setoid2_of_setoid1 (o1 ⇒_\r1 o2)) ≝ λo1,o2,x.x.
+
+interpretation "relation f⎻*" 'OR_f_minus_star r = (fun12 ?? (minus_star_image ? ?) (foo ?? r)).
+interpretation "relation f⎻" 'OR_f_minus r = (fun12 ?? (minus_image ? ?) (foo ?? r)).
+interpretation "relation f*" 'OR_f_star r = (fun12 ?? (star_image ? ?) (foo ?? r)).
definition image_coercion: ∀U,V:REL. (U ⇒_\r1 V) → Ω^U ⇒_2 Ω^V.
intros (U V r Us); apply (image U V r); qed.
exists; [apply a] split; [ change with (a = a); apply refl1 | assumption]]
qed.
-theorem minus_star_image_id: ∀o:REL. (fun12 ?? (minus_star_image o o) (id1 REL o) : carr2 (Ω^o ⇒_2 Ω^o)) =_1 (id2 SET1 Ω^o).
+theorem minus_star_image_id: ∀o:REL.
+ ((id1 REL o)⎻* : carr2 (Ω^o ⇒_2 Ω^o)) =_1 (id2 SET1 Ω^o).
intros; unfold minus_star_image; simplify; intro U; simplify;
split; simplify; intros;
[ change with (a ∈ U); apply f; change with (a=a); apply refl1
| cases f1; cases x1; apply f; assumption]
qed.
+
(*
(*CSC: unused! *)
theorem ext_comp:
| cases H; clear H; cases x1; clear x1; exists [apply w]; split;
[2: cases f] assumption]
qed.
+*)
+
+axiom daemon : False.
theorem extS_singleton:
- ∀o1,o2.∀a:arrows1 ? o1 o2.∀x.extS o1 o2 a (singleton o2 x) = ext o1 o2 a x.
+ ∀o1,o2.∀a.∀x.extS o1 o2 a {(x)} = ext o1 o2 a x.
intros; unfold extS; unfold ext; unfold singleton; simplify;
- split; intros 2; simplify; cases f; split; try assumption;
- [ cases H; cases x1; change in f2 with (eq1 ? x w); apply (. #‡f2 \sup -1);
- assumption
- | exists; try assumption; split; try assumption; change with (x = x); apply refl]
-qed.
-*)
+ split; intros 2; simplify; simplify in f;
+ [ cases f; cases e; cases x1; change in f2 with (x =_1 w); apply (. #‡f2); assumption;
+ | split; try apply I; exists [apply x] split; try assumption; change with (x = x); apply rule #;] qed.
\ No newline at end of file
definition powerset_of_POW': ∀A.oa_P (POW' A) → Ω^A ≝ λA,x.x.
coercion powerset_of_POW'.
-definition foo : ∀o1,o2:REL.carr1 (o1 ⇒_\r1 o2) → carr2 (setoid2_of_setoid1 (o1 ⇒_\r1 o2)) ≝ λo1,o2,x.x.
-
definition orelation_of_relation: ∀o1,o2:REL. o1 ⇒_\r1 o2 → (POW' o1) ⇒_\o2 (POW' o2).
intros;
constructor 1;
[ apply rule c;
- | apply rule ((foo ?? c)⎻* );
- | apply rule ((foo ?? c)* );
- | apply rule ((foo ?? c)⎻);
+ | apply rule (c⎻* );
+ | apply rule (c* );
+ | apply rule (c⎻);
| intros; split; intro;
[ intros 2; intros 2; apply (f y); exists[apply a] split; assumption;
| intros 2; change with (a ∈ q); cases f1; cases x; clear f1 x;
change in e with (t =_2 t'); unfold image_coercion; apply (†e);
qed.
-lemma minus_image_id : ∀o:REL.(foo ?? (id1 REL o))⎻ =_1 (id2 SET1 Ω^o).
+lemma minus_image_id : ∀o:REL.((id1 REL o))⎻ =_1 (id2 SET1 Ω^o).
unfold foo; intro o; intro; unfold minus_image; simplify; split; simplify; intros;
[ cases e; cases x; change with (a1 ∈ a); change in f with (a1 =_1 w);
apply (. f‡#); assumption;
change with (a1 =_1 a1); apply refl1;]
qed.
-lemma star_image_id : ∀o:REL. (foo ?? (id1 REL o))* =_1 (id2 SET1 Ω^o).
+lemma star_image_id : ∀o:REL. ((id1 REL o))* =_1 (id2 SET1 Ω^o).
unfold foo; intro o; intro; unfold star_image; simplify; split; simplify; intros;
[ change with (a1 ∈ a); apply f; change with (a1 =_1 a1); apply rule refl1;
| change in f1 with (a1 =_1 y); apply (. f1^-1‡#); apply f;]
[4: apply mem; |6: apply Hletin;|1,2,3,5: skip]
lapply (#‡prop11 ?? f ?? (†e)); [6: apply Hletin; |*:skip ]]
| (split; intro; split; simplify);
- (*
- whd; split; whd; intro; simplify; unfold map_arrows2; simplify;
- [ split;*)
[ change with (∀a1.(∀x. a1 ∈ (f {(x):S}) → x ∈ a) → a1 ∈ f⎻* a);
| change with (∀a1.a1 ∈ f⎻* a → (∀x.a1 ∈ f {(x):S} → x ∈ a));
| alias symbol "and" (instance 4) = "and_morphism".
projects / helm.git / commitdiff