# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: name-hunt: Union_of_singleton?

#### 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
```

#### Johan Commelin (Nov 26 2020 at 05:32):

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

#### 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.

#### Kenny Lau (Nov 26 2020 at 07:31):

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

#### Johan Commelin (Nov 26 2020 at 07:33):

Yup, you are totally right

#### 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
```

#### 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?

#### Eric Wieser (Nov 26 2020 at 08:44):

Should this lemma name contain the word subtype?

#### Eric Wieser (Nov 26 2020 at 09:18):

The non-subtype version is docs#set.bUnion_of_singleton

#### Eric Wieser (Nov 26 2020 at 09:18):

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

#### Eric Wieser (Nov 26 2020 at 09:28):

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

#### Kenny Lau (Nov 26 2020 at 09:47):

@Eric Wieser bad link (`set.set.`

)

#### Eric Wieser (Nov 26 2020 at 09:47):

Zulip needs the same linters as mathlib

#### 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).

#### 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⟩, })
```

#### 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...

#### 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],
```

#### 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