Stream: math-comp analysis

Topic: Is there lemmas for comparing sup/inf of different sets?

abab9579 (Sep 03 2022 at 13:58):

For instance, I would like following lemmas:

lem1: A `<=` B -> sup A <= sup B.
lem2: {homo f : x y / x <= y } -> sup (f `@ A) = f (sup A).
lem3: (forall x y x' y', x <= x' -> y <= y' -> f x y <= f x' y' ) -> sup [set f x y | x in A &  y in B] = f (sup A) (sup B)

Do these lemmas exist somewhere, or are they not present?

Pierre Roux (Sep 05 2022 at 12:05):

What does Search sup has_sup or Search sup (_ `<=` _) yields?

abab9579 (Sep 06 2022 at 03:02):

Oh, there is

le_sup:
  forall {R : realType} [S1 S2 : set R],
  S1 `<=` down (T:=R) S2 ->
  S1 !=set0 -> has_sup (T:=R) S2 -> sup S1 <= sup S2

However, I cannot find analogue for inf. How do I approach that one?

Reynald Affeldt (Sep 06 2022 at 03:45):

inf being defined as - sup (- A) it is maybe easy to prove the lemma you want using the properties of <= and -

abab9579 (Sep 06 2022 at 03:51):

Hmm, is it as easy to reason with-A and -B?

Reynald Affeldt (Sep 06 2022 at 03:57):

There are a number of lemmas about -%R @` E in reals.v.

Last updated: Feb 05 2023 at 15:03 UTC