## Stream: new members

### Topic: lemma in mathlib

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

#### 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

#### Kenny Lau (Dec 11 2020 at 15:21):

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

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

#### 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

#### 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

#### 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"?

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

#### 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

#### 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.)

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

#### Eric Wieser (Dec 11 2020 at 15:31):

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

#### 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

#### 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


#### 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

#### 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

#### Eric Wieser (Dec 11 2020 at 15:35):

I was expecting a lemma about lattices, not sets

#### Calle Sönne (Dec 11 2020 at 15:35):

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

#### Calle Sönne (Dec 11 2020 at 15:36):

but yeah then this could be stated more generally I guess

#### Eric Wieser (Dec 11 2020 at 15:36):

Sure, but this should be provable for all lattices

#### 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


#### Eric Wieser (Dec 11 2020 at 15:42):

Assuming it's true, anyway

#### 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

#### Calle Sönne (Dec 11 2020 at 15:42):

Eric Wieser said:

Assuming it's true, anyway

yeah

#### 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 :=


#### 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 :=


#### Eric Wieser (Dec 11 2020 at 15:45):

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

#### Eric Wieser (Dec 11 2020 at 15:57):

My statement was wrong

#### Eric Wieser (Dec 11 2020 at 15:57):

Should have been b not c

#### 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


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


#### 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

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

#### Eric Wieser (Dec 11 2020 at 16:24):

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

#### 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

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

#### 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

#### 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: Dec 20 2023 at 11:08 UTC