Supremums ereal #203
Supremums ereal #203
Conversation
affeldt-aist
force-pushed
the
supremums_ereal
branch
from
3126267
to
48661cc
Compare
|
@amahboubi @strub do you have an opinion about replacing |
|
@CohenCyril do you mean this commit f8d361a when you refer to the the new |
|
@CohenCyril so your opinion is to stick to |
|
(Trying to summarize.)
For the time being, this PR sticks to |
affeldt-aist
force-pushed
the
supremums_ereal
branch
from
76e89f1
to
31f83c2
Compare
|
As an additional piece of information about |
affeldt-aist
force-pushed
the
supremums_ereal
branch
from
f29b661
to
79880f9
Compare
|
We agreed on merging this PR during the last meeting but it seems that it incidentally implements one aspect of PR #117 (this was observed by @mkerjean ). @amahboubi Are you also ok with merging? |
- replace `pred` with `set` in `reals.v` and propagate - replace `-' E` by `-%R @' E`
- move Section ArchiBound from `reals.v` to `classical_sets.v` + could factorize the two definitions of `nonempty` - new lemmas `lee_ninfty_eq` and `lee_ninfty_eq` - new lemma `image_set0` in `classical_sets.v` - move `Section ERealOrderTheory` from `reals.v` to `ereal.v` - new `Section ereal_supremum` in `ereal.v` + Lemma `ereal_supremums_neq0` (sets of supremums of extended reals are not empty)
- replace `case`s of `pselect` with `have`s of `pselect`
- replace expressions such as `(forall y, X y -> (x <= y)%O)`
by `ub X` (resp. `lb`)
- avoid implicit unfolding of `ub`, `lb`, `down` by enforcing
usage of `ubP`, `lbP`, `downP`
+ in particular, change the definition of supremum to
`ub E `&` lb (ub E)`
- replace usage of `nonempty` by `!=set0`
- removed redundant `has_inP`, `has_supP`, `has_ubP`, `has_lbP`,
`nonemptyPn`
affeldt-aist
force-pushed
the
supremums_ereal
branch
from
79880f9
to
413e0c3
Compare
|
No objection. |
Thanks @amahboubi, I will merge then. |
The goal of this PR is to prove that a set of extended reals always has a supremum. For this purpose, I needed to generalize the definition of greatest elements, supremums, etc. from
reals.v. I tried for a while to stick to the originalpred-base definitions butsets fromclassical_sets.vturned out to be more handy and simplify proofs a bit.The first commit does the generalization, the second one adds the lemmas about extended reals.