finset.subset_iff_inter_eq_left / right

Stream: Is there code for X?

[Damiano Testa]

Dear All,

I needed the two lemmas below about finset that are the direct analogue of the corresponding lemmas on set. However, I was not able to find them. Is there a reason that they are not there? Should I make a PR to add them?

Do you also want to golf the proofs?

Thank you!

import data.finset.basic

namespace finset

theorem subset_iff_inter_eq_left {α : Type*} {s t : finset α} [decidable_eq α] :
  s ⊆ t ↔ s ∩ t = s :=
begin
  refine ⟨λ h, subset.antisymm (s.inter_subset_left t) (subset_inter (subset.refl s) h), λ h, _⟩,
  rw ← h,
  exact s.inter_subset_right t,
end

theorem subset_iff_inter_eq_right {α : Type*} {s t : finset α} [decidable_eq α] :
  s ⊆ t ↔ t ∩ s = s :=
by { rw inter_comm, exact subset_iff_inter_eq_left }

end finset

[Bryan Gin-ge Chen]

Both these and their set analogues should follow from something at the level of (semi)lattices, right? cf. docs#inf_eq_left

[Damiano Testa]

The set versions exist and they are set.subset_iff_inter_eq_left/right. I will try to make the proof work with lattices, thanks!

[Damiano Testa]

... the statement looks like the one that I want, but I am unable to convince Lean that ≤ = ⊆ and that ⊓ = ∩.

[Bryan Gin-ge Chen]

In #6775, I changed a bunch of finset and set proofs to use lattice / (generalized) Boolean algebra versions instead; most of the time Lean is able to see that ≤ and ⊆ are defeq, but sometimes I have to use show and some other tricks. Looking at the examples there might help

[Damiano Testa]

Indeed, thanks! This works:

theorem subset_iff_inter_eq_left {s t : finset α} [decidable_eq α] :
  s ⊆ t ↔ s ∩ t = s :=
(inf_eq_left.symm : s ≤ t ↔ s ⊓ t = s)

Now I am more doubtful: is this lemma worth a PR?

[Damiano Testa]

(Maybe with the two sides of the iff exchanged, to match the lattice version?)

[Bryan Gin-ge Chen]

I think so, at least judging by the existence of the set versions.

[Damiano Testa]

PR #7053

[Damiano Testa]

While placing these lemmas, I saw that the lattice instance is after a bunch of results that might also be proven via the lattice structure. Should these lemmas be reproven using lattice inf/sup stuff?

[Damiano Testa]

(I have not checked which ones of these lemmas are needed to get the lattice instance, I simply placed the two new ones after the instance and wondered...)

[Bryan Gin-ge Chen]

I noticed something similar when I was preparing #6775 and I wasn't sure either. It might be worth playing around with.

[Damiano Testa]

Ok, I will not do it in this PR, but, if this is something that should happen, I can add the comment

-- TODO: check which ones of these results now follow from the lattice structure

before the lemmas that might benefit from this. Maybe even at the beginning of the file, although the file is quite long.

[Damiano Testa]

CI successfully built the previous version did not finish yet!

However, I thought that it did and I added the TODO and I also flipped the iff's, since the subset side seems simpler than the side with the intersection and the equality.