lemma in mathlib

Stream: new members

[Calle Sönne]

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]

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]

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

[Calle Sönne]

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]

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

[Calle Sönne]

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]

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]

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]

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]

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]

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]

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

[Calle Sönne]

Eric Wieser said:

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

I will try to use this one then

[Eric Wieser]

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]

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]

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]

I was expecting a lemma about lattices, not sets

[Calle Sönne]

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

[Calle Sönne]

but yeah then this could be stated more generally I guess

[Eric Wieser]

Sure, but this should be provable for all lattices

[Eric Wieser]

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]

Assuming it's true, anyway

[Calle Sönne]

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]

Eric Wieser said:

Assuming it's true, anyway

yeah

[Calle Sönne]

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]

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]

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

[Eric Wieser]

My statement was wrong

[Eric Wieser]

Should have been b not c

[Eric Wieser]

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]

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]

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

[Calle Sönne]

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]

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

[Eric Wieser]

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]

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]

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]

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