Zulip Chat Archive

Stream: Is there code for X?

Topic: Canonical subsets of sum


view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Oct 13 2020 at 14:57):

range sum.inl?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 13 2020 at 15:01):

except for that one

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Adam Topaz (Oct 13 2020 at 15:03):

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

view this post on Zulip Mario Carneiro (Oct 13 2020 at 15:03):

there is a cases in the middle

view this post on Zulip Mario Carneiro (Oct 13 2020 at 15:03):

finish might get it

view this post on Zulip Adam Topaz (Oct 13 2020 at 15:03):

finish didn't work

view this post on Zulip Mario Carneiro (Oct 13 2020 at 15:03):

tidy?

view this post on Zulip Adam Topaz (Oct 13 2020 at 15:04):

yup!

view this post on Zulip Mario Carneiro (Oct 13 2020 at 15:04):

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

view this post on Zulip Adam Topaz (Oct 13 2020 at 15:04):

Yeah I tried with ext first.

view this post on Zulip Adam Topaz (Oct 13 2020 at 15:04):

BTW, is there an rcases analogue for ext?

view this post on Zulip Mario Carneiro (Oct 13 2020 at 15:04):

ext

view this post on Zulip Mario Carneiro (Oct 13 2020 at 15:05):

ext takes rcases patterns

view this post on Zulip Adam Topaz (Oct 13 2020 at 15:05):

Oh nice.

view this post on Zulip Adam Topaz (Oct 13 2020 at 15:06):

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

view this post on Zulip 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

docs#set.is_compl_range_inl_range_inr and docs#set.range_inl_union_range_inr


Last updated: May 07 2021 at 18:19 UTC