lemma placing contest

Stream: general

[Floris van Doorn]

I want to find a good home for the two lemmas below (or do similar lemmas already exist?). The first one first nicely in data.set.lattice, but the second one doesn't have a good place. Neither data.set.lattice or data.finset.lattice know about fintype.
Any suggestions?

import data.fintype.basic
open set

lemma Union_Inter_subset {ι ι' α} {s : ι → ι' → set α} : (⋃ j, ⋂ i, s i j) ⊆ ⋂ i, ⋃ j, s i j :=
by { rintro x ⟨_, ⟨i, rfl⟩, hx⟩ _ ⟨j, rfl⟩, exact ⟨_, ⟨i, rfl⟩, hx _ ⟨j, rfl⟩⟩ }

lemma Union_Inter_of_monotone {ι ι' α : Type*} [fintype ι] [decidable_linear_order ι']
  [nonempty ι'] {s : ι → ι' → set α} (hs : ∀ i, monotone (s i)) :
  (⋃ j : ι', ⋂ i : ι, s i j) = ⋂ i : ι, ⋃ j : ι', s i j :=
begin
  ext x, refine ⟨λ hx, Union_Inter_subset hx, λ hx, _⟩,
  simp only [mem_Inter, mem_Union, mem_Inter] at hx ⊢, choose j hj using hx,
  obtain ⟨j₀⟩ := show nonempty ι', by apply_instance,
  refine ⟨finset.univ.fold max j₀ j, λ i, hs i _ (hj i)⟩,
  rw [finset.fold_op_rel_iff_or (@le_max_iff _ _)],
  exact or.inr ⟨i, finset.mem_univ i, le_rfl⟩
end

[Floris van Doorn]

I guess I can put it in data.set.finite?

[Yury G. Kudryashov]

LGTM. BTW, the second lemma holds true if one of ι, ι' is nonempty.

[Anatole Dedecker]

I'm reviving this topic because I need these four lemmas, and I wanted to know (1) wether they deserve to go in mathlib (2) if so, where ? Thanks !

lemma bUnion_Iic_mono {ι α : Type*} [preorder ι] (φ : ι → set α) :
  monotone (λ (n : ι), ⋃ k (h : k ∈ Iic n), φ k) :=
λ i j hij, bUnion_subset_bUnion_left (λ k hk, le_trans hk hij)

lemma subset_bUnion_Iic {ι α : Type*} [preorder ι] (φ : ι → set α) (n : ι) :
  φ n ⊆ ⋃ k (h : k ∈ Iic n), φ k :=
subset_bUnion_of_mem right_mem_Iic

lemma bInter_Ici_mono {ι α : Type*} [preorder ι] (φ : ι → set α) :
  monotone (λ (n : ι), ⋂ k (h : k ∈ Ici n), φ k) :=
λ i j hij, bInter_subset_bInter_left (λ k hk, le_trans hij hk)

lemma bInter_Ici_subset {ι α : Type*} [preorder ι] (φ : ι → set α) (n : ι) :
  (⋂ k (h : k ∈ Ici n), φ k) ⊆ φ n :=
bInter_subset_of_mem left_mem_Ici

If it matters, I use them in #7164 : I have a few results for monotone families and I extend them to non monotone families by "squeezing" $\varphi_i$ between $\bigcap_{k\ge i} \varphi_k$ and $\bigcup_{k\le i} \varphi_k$

[Patrick Massot]

I think the second and fourth ones are not needed. They are direct combinations of two lemmas that are easy to find. The first and third one are a bit more tricky because of the le_trans bit that relies on the precise implementation of Iic. But I wouldn't be shocked to see all of them in mathlib, in data.set.intervals.

[Anatole Dedecker]

Actually I've just changed my mind on these :sweat_smile: I think they really feel too specific, and the "tricky" le.trans bit can be hidden behind Iic_subset_Iic. So I won't PR them, unless of course someone actively wants them in mathlib