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: 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)

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

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: Jun 22 2024 at 15:01 UTC