[Merged by Bors] - feat(order/sup_indep): More lemmas

[YaelDillies]

A few more lemmas about finset.sup_indep and set.pairwise_disjoint.

---

[fpvandoorn]

I also suggest making all the f's of type ι × ι' → α (and maybe the one in sup_indep.sigma explicit)

[eric-wieser]

It feels weird to have the pairwise_disjoint vesion of this before the disjoint version. Here's one disjoint version:

lemma disjoint.prod_left {α β : Type*} {f₁ f₂ : set α} (hf : disjoint f₁ f₂) (g₁ g₂ : set β) :
  disjoint (f₁ ×ˢ g₁) (f₂ ×ˢ g₂) :=
λ ⟨a, b⟩ ⟨⟨ha₁, hb₁⟩, ⟨ha₂, hb₂⟩⟩, hf ⟨ha₁, ha₂⟩

lemma disjoint.prod_right {α β : Type*} (f₁ f₂ : set α) {g₁ g₂ : set β} (hg : disjoint g₁ g₂) :
  disjoint (f₁ ×ˢ g₁) (f₂ ×ˢ g₂) :=
λ ⟨a, b⟩ ⟨⟨ha₁, hb₁⟩, ⟨ha₂, hb₂⟩⟩, hg ⟨hb₁, hb₂⟩

I'll let you think about what the analogous one for prod' is.

[YaelDillies]

I tried, but it doesn't seem to golf anything down.

[fpvandoorn]

LGTM

bors d+

[bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests