For instance, I would like following lemmas:

```
lem1: has_sup A -> has_sup B -> A `<=` B -> sup A <= sup B.
lem2: {homo f : x y / x <= y } -> has_sup A -> sup (f `@ A) = f (sup A).
lem3: (forall x y x' y', x <= x' -> y <= y' -> f x y <= f x' y' ) -> has_sup A -> has_sup B -> 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?

(Now thinking about it, latter two might not hold. Becomes true again if continuity condition is added)

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`

.

What about something along these lines?

```
Lemma lem1 (A B : set R) : has_sup A -> has_sup B -> A `<=` B -> sup A <= sup B.
Proof.
by move=> [A0 ?] hsB AB; apply: le_sup => //; exact: subset_trans (@le_down _).
Qed.
Lemma subsetN (A B : set R) : A `<=` B -> -%R @` A `<=` -%R @` B.
Proof. by move=> AB _ [x Bx <-]; exists x => //; exact: AB. Qed.
Lemma lem1' (A B : set R) : has_inf A -> has_inf B -> A `<=` B -> inf B <= inf A.
Proof.
by move=> hsA hsB AB; rewrite ler_oppr opprK; apply: lem1 => //;
[exact/has_inf_supN|exact/has_inf_supN|exact/subsetN].
Qed.
```

Oh, looks good! Thank you, I will use these lemmas.

abab9579 has marked this topic as resolved.

It does seem to me like e.g.

```
Lemma ex_image_sup_eq (f: R -> R) (A: set R) :
{mono f : x y / x <= y} -> has_sup A -> (range f) (sup (f @` A)) -> sup (f @` A) = f (sup A).
```

could be useful. (Although the `range f`

part need to be fleshed out)

Last updated: Jun 22 2024 at 15:01 UTC