Stream: Beginner Questions

Topic: Trichotomy


view this post on Zulip Artem Khovanov (Jul 15 2022 at 19:30):

Is there an easy way to specify logical dichotomy/trichotomy (ie exactly one of P,Q,R holds)?
If so, is there an intro rule for its cases?

view this post on Zulip Maximilian Schaeffeler (Jul 15 2022 at 19:56):

You might want to check out the command ˋconsiderˋ, e.g. in the Isabelle/Isar reference manual.

view this post on Zulip Artem Khovanov (Jul 15 2022 at 20:15):

Maximilian Schaeffeler said:

You might want to check out the command ˋconsiderˋ, e.g. in the Isabelle/Isar reference manual.

Perfect just what I wanted


Last updated: Mar 29 2024 at 08:18 UTC