Zulip Chat Archive

Stream: Is there code for X?

Topic: name-hunt: Union_of_singleton?


view this post on Zulip Damiano Testa (Nov 26 2020 at 04:49):

Dear All,

I have been unable to find the lemma below, but I would imagine that it is already in mathlib: do you know what is its name?

On a golfing technique, can you unify the rcases with exact?

Thank you!

import data.set.lattice

lemma setext {α : Type*} (s : set α) : s =  i : s , {i} :=
begin
--  ext1, simp,  also proves this lemma
  ext1 x,
  refine λ hx, set.mem_Union.mpr ⟨⟨x, hx⟩, rfl⟩, λ hx, _⟩,
  rcases set.mem_Union.mp hx with x, _, rfl⟩,
  exact subtype.val_prop x,
end

view this post on Zulip Johan Commelin (Nov 26 2020 at 05:32):

-- src/data/set/lattice.lean:438
@[simp] theorem sUnion_singleton (s : set α) : ⋃₀ {s} = s := Sup_singleton

view this post on Zulip Johan Commelin (Nov 26 2020 at 05:32):

atm, you can't combine rcases with exact. And I don't know how to turn it into a syntax that would really save many characters.

view this post on Zulip Kenny Lau (Nov 26 2020 at 07:31):

I don't think that is the theorem he's looking for?

view this post on Zulip Johan Commelin (Nov 26 2020 at 07:33):

Yup, you are totally right

view this post on Zulip Kenny Lau (Nov 26 2020 at 07:34):

import data.set.lattice

lemma setext {α : Type*} (s : set α) : s =  i : s , {i} :=
set.subset.antisymm (λ i his, set.mem_Union.2 ⟨⟨i, his⟩, rfl⟩) $
set.Union_subset $ λ i, set.singleton_subset_iff.2 i.2

view this post on Zulip Damiano Testa (Nov 26 2020 at 08:09):

Dear @Johan Commelin and @Kenny Lau , thank you for your inputs! Kenny's proof works for me! I do not know whether this lemma should be added to data.set.lattice. Do you have an opinion?

view this post on Zulip Eric Wieser (Nov 26 2020 at 08:44):

Should this lemma name contain the word subtype?

view this post on Zulip Eric Wieser (Nov 26 2020 at 09:18):

The non-subtype version is docs#set.bUnion_of_singleton

view this post on Zulip Eric Wieser (Nov 26 2020 at 09:18):

lemma setext {α : Type*} (s : set α) : s =  (i  s), {i} :=
(set.bUnion_of_singleton s).symm

view this post on Zulip Eric Wieser (Nov 26 2020 at 09:28):

docs#set.Union_of_singleton is also close, but it's missing the coercions

view this post on Zulip Kenny Lau (Nov 26 2020 at 09:47):

@Eric Wieser bad link (set.set.)

view this post on Zulip Eric Wieser (Nov 26 2020 at 09:47):

Zulip needs the same linters as mathlib

view this post on Zulip Damiano Testa (Nov 26 2020 at 10:44):

I do not necessarily insist on this lemma appearing in mathlib. I was simply surprised that it was not. However, it is a lemma that I am using and, so far, I have not been able to make the other suggestions work (except for Kenny's).

view this post on Zulip Eric Wieser (Nov 26 2020 at 10:56):

Perhaps this is the more useful lemma?

lemma set.Union_subtype {α : Type*} (s : set α) (f : α  set α) :
  ( (i : s), f i) =  (i  s), f i :=
set.subset.antisymm
  (λ x hx, by {
    obtain i, hi := set.mem_Union.mp hx,
    exact set.mem_Union.mpr i, set.mem_Union.mpr i.prop, hi⟩⟩, })
  (λ x hx, by {
    obtain i, hi := set.mem_Union.mp hx,
    obtain hi, hhi := set.mem_Union.mp hi,
    exact set.mem_Union.mpr ⟨⟨i, hi⟩, hhi⟩, })

view this post on Zulip Damiano Testa (Nov 26 2020 at 11:23):

For my actual example, I have not been able to use set.Union_subtype, though this is likely due to the fact that I am not understanding what is going on. I tried applying it with f given by λ i, singleton i and it did not work...

view this post on Zulip Eric Wieser (Nov 26 2020 at 11:55):

lemma setext {α : Type*} (s : set α) : s =  i : s , {i} :=
by rw [set.Union_subtype, set.bUnion_of_singleton],

view this post on Zulip Damiano Testa (Nov 26 2020 at 14:03):

@Eric Wieser this now works, thank you!

As I only use it once, I do not really have a strong opinion on which form of these lemmas to prefer, nor whether they "should be" in mathlib!

In any case, thank you all for your help!


Last updated: May 07 2021 at 22:14 UTC