Skip to content

Commit

Permalink
fix lee_pinfty and lee_ninfty
Browse files Browse the repository at this point in the history
  • Loading branch information
affeldt-aist committed Apr 26, 2020
1 parent 7364cbf commit 5fcd283
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions theories/ereal.v
Original file line number Diff line number Diff line change
Expand Up @@ -166,14 +166,14 @@ Proof. by []. Qed.
Lemma lte_pinfty (R : realDomainType) (x : R) : (x%:E < +oo).
Proof. exact: num_real. Qed.

Lemma lee_pinfty (R : realDomainType) (x : R) : (x%:E <= +oo).
Proof. by rewrite ltW // lte_pinfty. Qed.
Lemma lee_pinfty (R : realDomainType) (x : {ereal R}) : (x <= +oo).
Proof. case: x => //= r; exact: num_real. Qed.

Lemma lte_ninfty (R : realDomainType) (x : R) : (-oo < x%:E).
Proof. exact: num_real. Qed.

Lemma lee_ninfty (R : realDomainType) (x : R) : (-oo <= x%:E).
Proof. by rewrite ltW // lte_ninfty. Qed.
Lemma lee_ninfty (R : realDomainType) (x : {ereal R}) : (-oo <= x).
Proof. case: x => //= r; exact: num_real. Qed.

Section ERealOrder_realDomainType.
Context {R : realDomainType}.
Expand Down

0 comments on commit 5fcd283

Please sign in to comment.