- converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
- all_covered: ∀x: concr bp. x ⊩ form bp
+ converges: ∀a: carr1 (concr bp).∀U,V: carr1 (form bp). a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
+ all_covered: ∀x: carr1 (concr bp). x ⊩ form bp
- extS ?? rp \sub\c (BPextS CS2 (b ↓ c)) =
- BPextS CS1 ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f c));
+ minus_image ?? rp \sub\c (BPextS CS2 (b ↓ c)) =
+ BPextS CS1 ((minus_image ?? rp \sub\f b) ↓ (minus_image ?? rp \sub\f c));
definition convergent_relation_space_composition:
∀o1,o2,o3: concrete_space.
binary_morphism1
definition convergent_relation_space_composition:
∀o1,o2,o3: concrete_space.
binary_morphism1
apply (.= (extS_com ??????));
apply (.= (†(respects_converges ?????)));
apply (.= (respects_converges ?????));
apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1)));
apply refl1;
apply (.= (extS_com ??????));
apply (.= (†(respects_converges ?????)));
apply (.= (respects_converges ?????));
apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1)));
apply refl1;
apply (.= (extS_com ??????));
apply (.= (†(respects_all_covered ???)));
apply (.= respects_all_covered ???);
apply refl1]
| intros;
apply (.= (extS_com ??????));
apply (.= (†(respects_all_covered ???)));
apply (.= respects_all_covered ???);
apply refl1]
| intros;