Zulip Chat Archive

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