-(* the same as ⋄ for a basic pair *)
-definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
- intros; constructor 1;
- [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∃x:U. x ♮r y ∧ x ∈ S});
- intros; simplify; split; intro; cases H1; exists [1,3: apply w]
- [ apply (. (#‡H)‡#); assumption
- | apply (. (#‡H \sup -1)‡#); assumption]
- | intros; split; simplify; intros; cases H2; exists [1,3: apply w]
- [ apply (. #‡(#‡H1)); cases x; split; try assumption;
- apply (if ?? (H ??)); assumption
- | apply (. #‡(#‡H1 \sup -1)); cases x; split; try assumption;
- apply (if ?? (H \sup -1 ??)); assumption]]
-qed.
-
-(* the same as □ for a basic pair *)
-definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
- intros; constructor 1;
- [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∀x:U. x ♮r y → x ∈ S});
- intros; simplify; split; intros; apply H1;
- [ apply (. #‡H \sup -1); assumption
- | apply (. #‡H); assumption]
- | intros; split; simplify; intros; [ apply (. #‡H1); | apply (. #‡H1 \sup -1)]
- apply H2; [ apply (if ?? (H \sup -1 ??)); | apply (if ?? (H ??)) ] assumption]
-qed.
-
-(* minus_image is the same as ext *)
-
-theorem image_id: ∀o,U. image o o (id1 REL o) U = U.
- intros; unfold image; simplify; split; simplify; intros;
- [ change with (a ∈ U);
- cases H; cases x; change in f with (eq1 ? w a); apply (. f‡#); assumption
- | change in f with (a ∈ U);
- exists; [apply a] split; [ change with (a = a); apply refl | assumption]]
-qed.
-
-theorem minus_star_image_id: ∀o,U. minus_star_image o o (id1 REL o) U = U.
- intros; unfold minus_star_image; simplify; split; simplify; intros;
- [ change with (a ∈ U); apply H; change with (a=a); apply refl
- | change in f1 with (eq1 ? x a); apply (. f1 \sup -1‡#); apply f]
-qed.
-
-theorem image_comp: ∀A,B,C,r,s,X. image A C (r ∘ s) X = image B C r (image A B s X).
- intros; unfold image; simplify; split; simplify; intros; cases H; clear H; cases x;
- clear x; [ cases f; clear f; | cases f1; clear f1 ]
- exists; try assumption; cases x; clear x; split; try assumption;
- exists; try assumption; split; assumption.
-qed.
-
-theorem minus_star_image_comp:
- ∀A,B,C,r,s,X.
- minus_star_image A C (r ∘ s) X = minus_star_image B C r (minus_star_image A B s X).
- intros; unfold minus_star_image; simplify; split; simplify; intros; whd; intros;
- [ apply H; exists; try assumption; split; assumption
- | change with (x ∈ X); cases f; cases x1; apply H; assumption]
-qed.
-
-record continuous_relation (S,T: basic_topology) : Type ≝
- { cont_rel:> arrows1 ? S T;
- reduced: ∀U. U = J ? U → image ?? cont_rel U = J ? (image ?? cont_rel U);
- saturated: ∀U. U = A ? U → minus_star_image ?? cont_rel U = A ? (minus_star_image ?? cont_rel U)