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?

What does `Search sup has_sup`

or `Search sup (_ `<=` _)`

yields?

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?

`inf`

being defined as `- sup (- A)`

it is maybe easy to prove the lemma you want using the properties of `<=`

and `-`

Hmm, is it as easy to reason with`-A`

and `-B`

?

There are a number of lemmas about `-%R @` E`

in `reals.v`

.

Last updated: Feb 05 2023 at 15:03 UTC