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)
}.
-
+(*
definition continuous_relation_setoid: basic_topology → basic_topology → setoid1.
intros (S T); constructor 1;
[ apply (continuous_relation S T)
[2,4: intros; apply saturation_monotone; try (apply A_is_saturation); apply Hcut;]
apply Hcut2; assumption.
qed.
+*)
*)
\ No newline at end of file