``` ```

# Study of the class of weakly monotonic functions (Lemma 2.3)

``` Require Export Monotonic. Section Global.   Variable A: Type.   Section A.     Variables X Y: Type.     Variable TX: reduction_t A X.     Variable TY: reduction_t A Y. ```
weak monotonicity entails monotonicity
```     Lemma monotonic_wmonotonic: forall F, monotonic TX TY F -> wmonotonic TX TY F. ```
transitive, reflexive closure respects weak monotonicity
```     Lemma star_wmon: wmonotonic TX TX (star (X:=X)).     Variables F G: function X Y.     Hypothesis HF: wmonotonic TX TY F.     Hypothesis HG: wmonotonic TX TY G. ```
Composition respects weak monotonicity
```     Lemma Comp_wmon: wmonotonic TX TY (Comp G F). ```
Binary union respects weak monotonicity
```     Lemma Union2_wmon: wmonotonic TX TY (Union2 F G).     Section Union.       Variable I: Type.       Variable H: I -> function X Y.       Hypothesis HH: forall i, wmonotonic TX TY (H i). ```
Union respects weak monotonicity
```       Lemma Union_wmon: wmonotonic TX TY (Union H).     End Union.   End A.   Section B.     Variables X Y: Type.     Variable TX: reduction_t A X.     Variable TY: reduction_t A Y.     Variables F G: function X Y.     Hypothesis HF: wmonotonic TX TY F.     Hypothesis HG: wmonotonic TX TY G. ```
Iteration respects weak monotonicity
```     Lemma UExp_wmon: forall n, wmonotonic TX TY (fun R => UExp F R n).     Lemma UIter_wmon: wmonotonic TX TY (UIter F).   End B.   Section C.     Variables X Y: Type.     Variable TX: reduction_t A X.     Variable TY: reduction_t A Y.     Variables F G: function X X.     Hypothesis HF: wmonotonic TX TX F.     Hypothesis HG: wmonotonic TX TX G. ```
Chaining respects weak monotonicity
```     Lemma Chaining_wmon: wmonotonic TX TX (Chain F G).     Variable L: relation Y.     Hypothesis HL: simulation TY TY L. ```
The following lemma is not a consequence of the previous one, for typing reasons
```     Lemma chaing_l_wmon: wmonotonic TY TX (chaining_l L).   End C. End Global. ```