abab9579 (Sep 03 2022 at 13:58): 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.
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: Oct 13 2024 at 01:02 UTC