Topic: Empty or not empty
Patrick Massot (Dec 17 2018 at 10:31):
How can I prove something by case splitting depending on whether or not a type is inhabited? I know about the
nonempty classes, but it looks like I can't do anything when I assume
not (nonempty a) or
not (inhabited a). So what I do is
by_cases H : ∃ x : α, true,. Is that right?
Chris Hughes (Dec 17 2018 at 10:38):
You can prove
a -> false from
h : not (nonempty a), it's just
assume x, h ⟨x⟩. Not sure what else you'd need apart from this.
Patrick Massot (Dec 17 2018 at 10:41):
Strange, I thought I tried that. Thanks! I does look slightly less stupid that way
Last updated: May 10 2021 at 19:16 UTC