## Stream: Is there code for X?

### Topic: Canonical subsets of sum

#### Adam Topaz (Oct 13 2020 at 14:51):

Does mathlib have some nice notation/abbreviation for the two canonical subsets of a disjoint union of types?
Specifically for the following two sets:

variables {α β : Type}
example : set (α ⊕ β) := sum.inl '' set.univ
example : set (α ⊕ β) := sum.inr '' set.univ


#### Yury G. Kudryashov (Oct 13 2020 at 14:57):

range sum.inl?

#### Adam Topaz (Oct 13 2020 at 14:58):

Oh yeah I always forget about range. But I still feel like there should be some smaller notation, like sum.setl and sum.setr.

#### Adam Topaz (Oct 13 2020 at 15:01):

This lemma also seems to be missing... (at least library search didn't find it).

variables {α β : Type}
example : (set.range sum.inl : set (α ⊕ β)) ∪ (set.range sum.inr) = set.univ := sorry


#### Mario Carneiro (Oct 13 2020 at 15:01):

I don't think it pulls its weight; you would have to unfold the definition to do anything with it, and it doesn't really have any interesting theorems that aren't easily expressible with range

#### Mario Carneiro (Oct 13 2020 at 15:01):

except for that one

#### Adam Topaz (Oct 13 2020 at 15:02):

Mario Carneiro said:

I don't think it pulls its weight; you would have to unfold the definition to do anything with it, and it doesn't really have any interesting theorems that aren't easily expressible with range

Fair enough...

#### Mario Carneiro (Oct 13 2020 at 15:02):

I don't think the lemma is there, but it's not hard to prove. There are similar theorems for prod and option too

#### Adam Topaz (Oct 13 2020 at 15:03):

I'm surprised that tauto doesn't immediately prove it!

#### Mario Carneiro (Oct 13 2020 at 15:03):

there is a cases in the middle

#### Mario Carneiro (Oct 13 2020 at 15:03):

finish might get it

#### Adam Topaz (Oct 13 2020 at 15:03):

finish didn't work

tidy?

yup!

#### Mario Carneiro (Oct 13 2020 at 15:04):

finish needs you to make the first move btw, applying set.ext

#### Adam Topaz (Oct 13 2020 at 15:04):

Yeah I tried with ext first.

#### Adam Topaz (Oct 13 2020 at 15:04):

BTW, is there an rcases analogue for ext?

#### Mario Carneiro (Oct 13 2020 at 15:04):

ext

#### Mario Carneiro (Oct 13 2020 at 15:05):

ext takes rcases patterns

Oh nice.

#### Adam Topaz (Oct 13 2020 at 15:06):

Okay, so now I have 17 different proofs of this very serious lemma.

#### Yury G. Kudryashov (Oct 13 2020 at 15:39):

Mario Carneiro said:

I don't think the lemma is there, but it's not hard to prove. There are similar theorems for prod and option too

Last updated: May 07 2021 at 18:19 UTC