diff options
| author | Vincent Semeria | 2020-03-01 17:30:57 +0100 |
|---|---|---|
| committer | Vincent Semeria | 2020-03-27 18:30:38 +0100 |
| commit | ad91d136b8d51e859ce3b959674757818e753bcb (patch) | |
| tree | dfa53ed5e7e5ade626f389b626d787263b028f68 /theories/Reals/Raxioms.v | |
| parent | 7ba059507b67b1f6ea3566a5d1dee40f6af78316 (diff) | |
Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move ConstructiveReals into new directory Abstract. Remove imports of implementations inside those Abstract files.
Add changelog for constructive reals cleanup
Move Cauchy reals into new directory Cauchy
Update stdlib index
Rename sum_f_R0
Use coqdoc comments
Update doc/changelog/10-standard-library/11725-cleanup-reals.rst
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
Update doc/changelog/10-standard-library/11725-cleanup-reals.rst
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
Update doc/changelog/10-standard-library/11725-cleanup-reals.rst
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
Improve notations
Diffstat (limited to 'theories/Reals/Raxioms.v')
| -rw-r--r-- | theories/Reals/Raxioms.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 57912a1196..8c5bc8475b 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -24,7 +24,7 @@ Require Import ClassicalDedekindReals. Require Import ConstructiveCauchyReals. Require Import ConstructiveCauchyRealsMult. Require Import ConstructiveRcomplete. -Require Import ConstructiveRealsLUB. +Require Import ConstructiveLUB. Require Export Rdefinitions. Local Open Scope R_scope. @@ -438,7 +438,7 @@ Proof. as Ebound. { destruct H. exists (Rrepr x). intros y Ey. rewrite <- (Rquot2 y). apply Rrepr_le. apply H. exact Ey. } - destruct (CR_sig_lub CRealImplem + destruct (@CR_sig_lub CRealConstructive Er Erproper sig_forall_dec sig_not_dec Einhab Ebound). exists (Rabst x). split. intros y Ey. apply Rrepr_le. rewrite Rquot2. |