Zulip Chat Archive
Stream: maths
Topic: disjoint union
Jester Cabading (Jul 09 2025 at 17:39):
where can I find the notion of disjoint union in mathlib?
Aaron Liu (Jul 09 2025 at 17:41):
which disjoint union?
Aaron Liu (Jul 09 2025 at 17:42):
docs#Sum is the disjoint union of types
Kenny Lau (Jul 09 2025 at 17:42):
Jester Cabading said:
where can I find the notion of disjoint union in mathlib?
in type theory, it's called sigma type, you type that with a big sigma \S
Notification Bot (Jul 09 2025 at 20:45):
4 messages were moved here from #maths > Representation Theory by Kevin Buzzard.
Last updated: Dec 20 2025 at 21:32 UTC