Zulip Chat Archive

Stream: new members

Topic: cases/exists


view this post on Zulip Iocta (Jul 28 2020 at 22:07):

Documentation says cases x works on an instance x of an inductive type. What is the inductive type in cases h ((u n - l)/2) in this solution?

view this post on Zulip Jalex Stark (Jul 28 2020 at 22:09):

it's something like \exists N, hN

view this post on Zulip Anatole Dedecker (Jul 28 2020 at 22:09):

The full thing we apply cases to is h ((u n - l)/2) (by linarith). If you want to see its type, you can just insert a line have := h ((u n - l)/2) (by linarith), and see the type of this in the tactic state

view this post on Zulip Iocta (Jul 28 2020 at 22:11):

this :  (N : ),  (n_1 : ), n_1  N  |u n_1 - l|  (u n - l) / 2

view this post on Zulip Jalex Stark (Jul 28 2020 at 22:12):

that looks right; are you still confused about something?

view this post on Zulip Iocta (Jul 28 2020 at 22:13):

What is inductive about it?

view this post on Zulip Jalex Stark (Jul 28 2020 at 22:16):

\exists is an inductive constructor

view this post on Zulip Jalex Stark (Jul 28 2020 at 22:16):

so are \and and \or

view this post on Zulip Patrick Massot (Jul 28 2020 at 22:16):

https://leanprover-community.github.io/mathlib_docs/core/init/logic.html#Exists

view this post on Zulip Bryan Gin-ge Chen (Jul 28 2020 at 22:18):

Relevant TPiL section

view this post on Zulip Iocta (Jul 28 2020 at 22:19):

thanks, will review that


Last updated: May 09 2021 at 20:11 UTC