compatibility: ∀U,V. (A U ≬ J V) = (U ≬ J V)
}.
-lemma hint: basic_topology → objs1 REL.
- intro; apply (carrbt b);
-qed.
-coercion hint.
-
record continuous_relation (S,T: basic_topology) : Type1 ≝
{ cont_rel:> arrows1 ? S T;
reduced: ∀U. U = J ? U → image ?? cont_rel U = J ? (image ?? cont_rel U);
| simplify; intros; apply trans1; [2: apply H |3: apply H1; |1: skip]]]
qed.
-definition cont_rel': ∀S,T: basic_topology. continuous_relation_setoid S T → arrows1 ? S T ≝ cont_rel.
-
-coercion cont_rel'.
-
-definition cont_rel'': ∀S,T: basic_topology. continuous_relation_setoid S T → binary_relation S T ≝ cont_rel.
-
-coercion cont_rel''.
-
theorem continuous_relation_eq':
∀o1,o2.∀a,a': continuous_relation_setoid o1 o2.
a = a' → ∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X).