Commit 1574e8c2 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added theorems about reflexivity of standard predicates.

parent c8016fa9
......@@ -201,6 +201,18 @@ rewrite Ropp_involutive.
apply H1.
Qed.
Theorem Rnd_DN_pt_refl :
forall F : R -> Prop,
forall x : R, F x ->
Rnd_DN_pt F x x.
Proof.
intros F x Hx.
repeat split.
exact Hx.
apply Rle_refl.
now intros.
Qed.
Theorem Rnd_DN_pt_idempotent :
forall F : R -> Prop,
forall x f : R,
......@@ -229,6 +241,18 @@ intros x Hx.
now apply Rnd_DN_pt_idempotent with (2 := Hx).
Qed.
Theorem Rnd_UP_pt_refl :
forall F : R -> Prop,
forall x : R, F x ->
Rnd_UP_pt F x x.
Proof.
intros F x Hx.
repeat split.
exact Hx.
apply Rle_refl.
now intros.
Qed.
Theorem Rnd_UP_pt_idempotent :
forall F : R -> Prop,
forall x f : R,
......@@ -551,6 +575,20 @@ rewrite Hxy.
apply Rle_refl.
Qed.
Theorem Rnd_N_pt_refl :
forall F : R -> Prop,
forall x : R, F x ->
Rnd_N_pt F x x.
Proof.
intros F x Hx.
repeat split.
exact Hx.
intros g _.
unfold Rminus at 1.
rewrite Rplus_opp_r, Rabs_R0.
apply Rabs_pos.
Qed.
Theorem Rnd_N_pt_idempotent :
forall F : R -> Prop,
forall x f : R,
......@@ -884,6 +922,20 @@ intros F rnd Hr x y Hxy.
now apply Rnd_NA_pt_monotone with F.
Qed.
Theorem Rnd_NA_pt_refl :
forall F : R -> Prop,
forall x : R, F x ->
Rnd_NA_pt F x x.
Proof.
intros F x Hx.
split.
now apply Rnd_N_pt_refl.
intros f Hxf.
apply Req_le.
apply f_equal.
now apply Rnd_N_pt_idempotent with (1 := Hxf).
Qed.
Theorem Rnd_NA_pt_idempotent :
forall F : R -> Prop,
forall x f : R,
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment