(* These are only conversions :-) *)
-definition o_operator_of_operator:
- ∀C:REL. (Ω \sup C => Ω \sup C) → (SUBSETS C ⇒ SUBSETS C).
- intros (C t);apply t;
-qed.
+definition o_operator_of_operator: ∀C:REL. (Ω^C ⇒_1 Ω^C) → ((POW C) ⇒_1 (POW C)) ≝ λC,t.t.
-definition is_o_saturation_of_is_saturation:
- ∀C:REL.∀R: unary_morphism1 (Ω \sup C) (Ω \sup C).
- is_saturation ? R → is_o_saturation ? (o_operator_of_operator ? R).
- intros; apply i;
-qed.
+definition is_o_saturation_of_is_saturation:
+ ∀C:REL.∀R: Ω^C ⇒_1 Ω^C. is_saturation ? R → is_o_saturation ? (o_operator_of_operator ? R).
+intros (C R i); apply i; qed.
-definition is_o_reduction_of_is_reduction:
- ∀C:REL.∀R: unary_morphism1 (Ω \sup C) (Ω \sup C).
- is_reduction ? R → is_o_reduction ? (o_operator_of_operator ? R).
- intros; apply i;
-qed.
\ No newline at end of file
+definition is_o_reduction_of_is_reduction:
+ ∀C:REL.∀R: Ω^C ⇒_1 Ω^C.is_reduction ? R → is_o_reduction ? (o_operator_of_operator ? R).
+intros (C R i); apply i; qed.