Zulip Chat Archive

Stream: general

Topic: lemma placing contest


Floris van Doorn (Sep 29 2020 at 02:39):

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 (Sep 29 2020 at 02:41):

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

Yury G. Kudryashov (Sep 29 2020 at 03:20):

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

Anatole Dedecker (Jun 13 2021 at 14:32):

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" φi\varphi_i between kiφk\bigcap_{k\ge i} \varphi_k and kiφk\bigcup_{k\le i} \varphi_k

Patrick Massot (Jun 13 2021 at 16:46):

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 (Jun 13 2021 at 20:00):

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


Last updated: Dec 20 2023 at 11:08 UTC