## Stream: math-comp analysis

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

#### Reynald Affeldt (Sep 06 2022 at 04:23):

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.
``````

#### abab9579 (Sep 06 2022 at 04:36):

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

#### Notification Bot (Sep 06 2022 at 04:36):

abab9579 has marked this topic as resolved.

#### abab9579 (Sep 07 2022 at 06:47):

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: Jan 30 2023 at 11:03 UTC