Stream: math-comp analysis

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


view this post on Zulip 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)

view this post on Zulip Pierre Roux (Sep 05 2022 at 12:05):

What does Search sup has_sup or Search sup (_ `<=` _) yields?

view this post on Zulip 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?

view this post on Zulip 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 -

view this post on Zulip abab9579 (Sep 06 2022 at 03:51):

Hmm, is it as easy to reason with-A and -B?

view this post on Zulip Reynald Affeldt (Sep 06 2022 at 03:57):

There are a number of lemmas about -%R @` E in reals.v.

view this post on Zulip 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.

view this post on Zulip abab9579 (Sep 06 2022 at 04:36):

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

view this post on Zulip Notification Bot (Sep 06 2022 at 04:36):

abab9579 has marked this topic as resolved.

view this post on Zulip 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