Zulip Chat Archive

Stream: new members

Topic: lemma in mathlib


view this post on Zulip Calle Sönne (Dec 11 2020 at 15:20):

Does anyone know of a lemma like the following in mathlib:

lemma subset_refined_of_subset_disjoint_cover {α : Type*} {Z a b u v : set α} (hZ : Z  u)
  (hbv : b  v) (Zab : Z  a  b) (huv : u  v = ) : Z  a :=

I have looked through the partitions file, but there doesnt seem to be anything like this in there. Is there some name for lemmas about "disjoint covers by two sets" in lean? I am really not sure what to search to find this.

view this post on Zulip Calle Sönne (Dec 11 2020 at 15:21):

Calle Sönne said:

Does anyone know of a lemma like the following in mathlib:

lemma subset_refined_of_subset_disjoint_cover {α : Type*} {Z a b u v : set α} (hZ : Z  u)
  (hbv : b  v) (Zab : Z  a  b) (huv : u  v = ) : Z  a :=

I have looked through the partitions file, but there doesnt seem to be anything like this in there. Is there some name for lemmas about "disjoint covers by two sets" in lean? I am really not sure what to search to find this.

I have proven this lemma myself, but I want to PR some code into mathlib so if there exists a framework for working with situations like these I should probably rewrite some of my code to use that instead

view this post on Zulip Kenny Lau (Dec 11 2020 at 15:21):

I would just prove it by hand, this looks like a very specific lemma

view this post on Zulip Calle Sönne (Dec 11 2020 at 15:22):

Kenny Lau said:

I would just prove it by hand, this looks like a very specific lemma

Yeah. And where would it go in mathlib? I would like to keep this as a separate lemma because it feels like this will be useful when working with normal spaces.

view this post on Zulip Calle Sönne (Dec 11 2020 at 15:22):

Because then you often end up with the situation of having a "refinement" of a disjoint cover

view this post on Zulip Calle Sönne (Dec 11 2020 at 15:24):

I guess what Im trying to say is that it feels like the statement should go in separation.lean (where the stuff about normal spaces is). But then again the statement itself has nothing to do with topological spaces

view this post on Zulip Eric Wieser (Dec 11 2020 at 15:26):

What did your proof look like? Perhaps a better question is "can I write this proof in terms of one or two lemmas that already exist"?

view this post on Zulip Kevin Buzzard (Dec 11 2020 at 15:26):

Kenny is arguing that this is not suitable for inclusion in a maths library, because there are probably 50 other lemmas of this complexity and the basic tools you need to prove it (Z in a union b and b in v so Z in a union v, u intersect v empty and Z in u so Z intersect v empty, Z in a union v and Z intersect v empty so Z in a) are probably all there already.

view this post on Zulip Calle Sönne (Dec 11 2020 at 15:27):

Kevin Buzzard said:

Kenny is arguing that this is not suitable for inclusion in a maths library, because there are probably 50 other lemmas of this complexity and the basic tools you need to prove it (Z in a union b and b in v so Z in a union v, u intersect v empty and Z in u so Z intersect v empty, Z in a union v and Z intersect v empty so Z in a) are probably all there already.

ah so I should just make a "have" statement or something in my main lemma for this, and then prove it there

view this post on Zulip Calle Sönne (Dec 11 2020 at 15:28):

Eric Wieser said:

What did your proof look like? Perhaps a better question is "can I write this proof in terms of one or two lemmas that already exist"?

It used set.subset_compl_iff_disjoint a bunch. The rest is just basic set theory operations (transitivity of subset, intersections is commutative etc.)

view this post on Zulip Calle Sönne (Dec 11 2020 at 15:30):

Kevin Buzzard said:

Kenny is arguing that this is not suitable for inclusion in a maths library, because there are probably 50 other lemmas of this complexity and the basic tools you need to prove it (Z in a union b and b in v so Z in a union v, u intersect v empty and Z in u so Z intersect v empty, Z in a union v and Z intersect v empty so Z in a) are probably all there already.

Also I need to use it twice in my main lemma, so the initial reason I made it a separate lemma was to decrease the amount of code.

view this post on Zulip Eric Wieser (Dec 11 2020 at 15:31):

I think docs#disjoint.mono is most of your proof

view this post on Zulip Calle Sönne (Dec 11 2020 at 15:32):

Eric Wieser said:

I think docs#disjoint.mono is most of your proof

I will try to use this one then

view this post on Zulip Eric Wieser (Dec 11 2020 at 15:32):

lemma subset_refined_of_subset_disjoint_cover {α : Type*} {Z a b u v : set α} (hZ : Z  u)
  (hbv : b  v) (Zab : Z  a  b) (huv : disjoint u v) : Z  a :=
begin
  replace Zab : Z  a  b := Zab,
  replace hbv : b  v := hbv,
  replace hZ : Z  u := hZ,
  have := huv.mono hZ hbv,
  change Z  a,
  clear hZ hbv huv,
  sorry
end

view this post on Zulip Eric Wieser (Dec 11 2020 at 15:34):

Goal state is

Zab: Z  a  b
this: disjoint Z b
 Z  a

which looks easy, but I haven't found the lemma for

view this post on Zulip Calle Sönne (Dec 11 2020 at 15:35):

Eric Wieser said:

Goal state is

Zab: Z  a  b
this: disjoint Z b
 Z  a

which looks easy, but I haven't found the lemma for

set.subset_compl_iff_disjoint should help

view this post on Zulip Eric Wieser (Dec 11 2020 at 15:35):

I was expecting a lemma about lattices, not sets

view this post on Zulip Calle Sönne (Dec 11 2020 at 15:35):

oh. I though lean would remember that we are working with lattices "that are sets"

view this post on Zulip Calle Sönne (Dec 11 2020 at 15:36):

but yeah then this could be stated more generally I guess

view this post on Zulip Eric Wieser (Dec 11 2020 at 15:36):

Sure, but this should be provable for all lattices

view this post on Zulip Eric Wieser (Dec 11 2020 at 15:39):

I think this might make a good lemma

-- or is this right_sup?
lemma disjoint.left_sup {α : Type*} [_inst_1 : complete_lattice α] {a b c : α} (h : a  b  c) (h : disjoint a c):
    a  c := by library_search

view this post on Zulip Eric Wieser (Dec 11 2020 at 15:42):

Assuming it's true, anyway

view this post on Zulip Calle Sönne (Dec 11 2020 at 15:42):

Eric Wieser said:

I think this might make a good lemma

-- or is this right_sup?
lemma disjoint.left_sup {α : Type*} [_inst_1 : complete_lattice α] {a b c : α} (h : a  b  c) (h : disjoint a c):
    a  c := by library_search

If it is true, in my head the reason for why it holds uses complements

view this post on Zulip Calle Sönne (Dec 11 2020 at 15:42):

Eric Wieser said:

Assuming it's true, anyway

yeah

view this post on Zulip Calle Sönne (Dec 11 2020 at 15:43):

there is this in the complement case, but maybe you knew about it already:

lemma disjoint_left_iff (h : is_compl y z) : disjoint x y  x  z :=

view this post on Zulip Calle Sönne (Dec 11 2020 at 15:45):

Oh this looks promising

lemma inf_eq_bot_iff_le_compl {α : Type u} [bounded_distrib_lattice α] {a b c : α}
  (h₁ : b  c = ) (h₂ : b  c = ) : a  b =   a  c :=

view this post on Zulip Eric Wieser (Dec 11 2020 at 15:45):

complete_lattice may be too weak, I don't know my lattices

view this post on Zulip Eric Wieser (Dec 11 2020 at 15:57):

My statement was wrong

view this post on Zulip Eric Wieser (Dec 11 2020 at 15:57):

Should have been b not c

view this post on Zulip Eric Wieser (Dec 11 2020 at 15:58):

lemma disjoint.left_sup {α : Type*} [bounded_distrib_lattice α] {a b c : α} (h : a  b  c) (hd : disjoint a c):
    a  b :=
begin
  have := inf_le_inf_left a h,
  rw [inf_idem, inf_sup_left, disjoint_iff.mp hd, sup_bot_eq, le_inf_iff] at this,
  exact this.2,
end

view this post on Zulip Eric Wieser (Dec 11 2020 at 16:13):

Golfed:

lemma disjoint.left_sup {α : Type*} [bounded_distrib_lattice α] {a b c : α} (h : a  b  c) (hd : disjoint a c):
  a  b :=
(λ x, le_of_inf_le_sup_le x (sup_le h le_sup_right)) ((disjoint_iff.mp hd).symm  bot_le)

view this post on Zulip Eric Wieser (Dec 11 2020 at 16:14):

This golf is a weird one - I need the lambda for elaboration to work out the types in the right order

view this post on Zulip Calle Sönne (Dec 11 2020 at 16:24):

Eric Wieser said:

Golfed:

lemma disjoint.left_sup {α : Type*} [bounded_distrib_lattice α] {a b c : α} (h : a  b  c) (hd : disjoint a c):
  a  b :=
(λ x, le_of_inf_le_sup_le x (sup_le h le_sup_right)) ((disjoint_iff.mp hd).symm  bot_le)

Oh I didnt know this existed: ▸ :joy: Now I can do a lot more in term mode proofs! Thank you for the help :)

view this post on Zulip Eric Wieser (Dec 11 2020 at 16:24):

Note that the pickiness of the triangle is why I had to use the lambda

view this post on Zulip Eric Wieser (Dec 11 2020 at 16:24):

Also I think you probably want a different name for that lemma than what I have, given that docs#disjoint_sup_left and docs#disjoint.sup_left already exist

view this post on Zulip Eric Wieser (Dec 11 2020 at 16:26):

Perhaps disjoint.left_le_of_le_sup_right (h : a ≤ b ⊔ c) and disjoint.left_le_of_le_sup_left (h : a ≤ c ⊔ b) or something like that, where the first left is because it's the left argument of disjoint.

view this post on Zulip Calle Sönne (Dec 11 2020 at 20:49):

Eric Wieser said:

Perhaps disjoint.left_le_of_le_sup_right (h : a ≤ b ⊔ c) and disjoint.left_le_of_le_sup_left (h : a ≤ c ⊔ b) or something like that, where the first left is because it's the left argument of disjoint.

I played around a bit with the left case and this was the best I could come up with:

lemma disjoint.left_le_of_le_sup_left {α : Type*} [bounded_distrib_lattice α] {a b c : α} (h : a  c  b) (hd : disjoint a c):
  a  b :=
@le_of_inf_le_sup_le _ _ a b c ((disjoint_iff.mp hd).symm  bot_le) ((@sup_comm _ _ c b)  (sup_le h le_sup_left))

Had to use eq.subst twice which was why I couldnt get your trick for the first one to work. So if I understood correctly, the problem with ▸ is that it does not allow any metavariables in any of the arguments and goal right? Thats why I manually gave le_of_inf_le_sup_leits arguments, but also sup_comm since there seemed to be no way of those being inferred before is applied

view this post on Zulip Calle Sönne (Dec 11 2020 at 20:50):

Also after playing around with it for a bit I realised that your solution with the lambda is pretty clever :)


Last updated: May 14 2021 at 04:22 UTC