-definition comprehension: ∀b:REL. (b ⇒ CPROP) → Ω \sup b.
- apply (λb:REL. λP: b ⇒ CPROP. {x | x ∈ b ∧ P x});
- intros; simplify; apply (.= (H‡#)‡(†H)); apply refl1.
-qed.
-
-interpretation "subset comprehension" 'comprehension s p =
- (comprehension s (mk_unary_morphism __ p _)).
-
-definition ext: ∀X,S:REL. ∀r: arrows1 ? X S. S ⇒ Ω \sup X.
- apply (λX,S,r.mk_unary_morphism ?? (λf.{x ∈ X | x ♮r f}) ?);
- [ intros; simplify; apply (.= (H‡#)); apply refl1
- | intros; simplify; split; intros; simplify; intros;
- [ apply (. #‡(#‡H)); assumption
- | apply (. #‡(#‡H\sup -1)); assumption]]
-qed.
-
-definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup 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
- |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;
- [1,3: assumption
- |2,4: exists; [1,3: apply w]
- [ apply (. (#‡H)‡#); assumption
- | apply (. (#‡H\sup -1)‡#); assumption]]]
-qed.
-
-definition fintersects: ∀o: basic_pair. form o → form o → Ω \sup (form o).
- apply
- (λo: basic_pair.λa,b: form o.
- {c | ext ?? (rel o) c ⊆ ext ?? (rel o) a ∩ ext ?? (rel o) b });
- intros; simplify; apply (.= (†H)‡#); apply refl1.
-qed.
-
-interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
-
-definition fintersectsS:
- ∀o:basic_pair. Ω \sup (form o) → Ω \sup (form o) → Ω \sup (form o).
- apply (λo: basic_pair.λa,b: Ω \sup (form o).
- {c | ext ?? (rel o) c ⊆ extS ?? (rel o) a ∩ extS ?? (rel o) b });
- intros; simplify; apply (.= (†H)‡#); apply refl1.
-qed.
-
-interpretation "fintersectsS" 'fintersects U V = (fintersectsS _ U V).
-
-(*
-definition relS: ∀o: basic_pair. concr o → Ω \sup (form o) → CProp.
- apply (λo:basic_pair.λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y);
-
-interpretation "basic pair relation for subsets" 'Vdash2 x y = (relS _ x y).
-interpretation "basic pair relation for subsets (non applied)" 'Vdash = (relS _).
-
-record concrete_space : Type ≝
- { bp:> basic_pair;
- converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
- all_covered: ∀x: concr bp. x ⊩ form bp