[real] sup/inf lemmas using set notations

[binghe]

Hi,

It's a little strange that, in realTheory, the sup and inf of set of real numbers, definitions and lemmas are not using set notations at all. Instead of, P x is used instead of x IN P and ?x. P x is used instead of P <> {}, etc. I found these lemmas hard to use, especially when the involved sets are defined in gspec notations (e.g. {x | P x}, the simplifier can rewrite x IN {x | P x} but cannot deal with the equivalent {x | P x} x.

Therefore now I added a variant for each of these lemmas using set notations (the "primed" version is new):

   [REAL_SUP_UBOUND]  Theorem (existing)
      ⊢ ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒ ∀y. P y ⇒ y ≤ sup P
   
   [REAL_SUP_UBOUND']  Theorem (new)
      ⊢ ∀P. P ≠ ∅ ∧ (∃z. ∀x. x ∈ P ⇒ x < z) ⇒ ∀y. y ∈ P ⇒ y ≤ sup P
   
   [REAL_SUP_UBOUND_LE]  Theorem (existing)
      ⊢ ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x ≤ z) ⇒ ∀y. P y ⇒ y ≤ sup P
   
   [REAL_SUP_UBOUND_LE']  Theorem (new)
      ⊢ ∀P. P ≠ ∅ ∧ (∃z. ∀x. x ∈ P ⇒ x ≤ z) ⇒ ∀y. y ∈ P ⇒ y ≤ sup P

Perhaps the original intent was to prevent explicitly using pred_setTheory but this is no more any issue. Also, the versions of set notation is actually more foundamental. If we were having these lemmas with set notations, the original versions can be obtained by a simple rewrite with IN_APP and GSYM MEMBER_NOT_EMPTY. The other side of rewriting is impossible (or hard), because all lambda-applications x y can be interpreted as y IN x.

P.S. In extrealTheory (or extreal_baseTheory), the original sup/inf lemmas are also in similar shapes, and I have already added a lot of such variants using set notations (and then use them in new probability proofs).

Chun

[mn200]

Thanks for this!