Zulip Chat Archive

Stream: general

Topic: Empty or not empty


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

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

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