## 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