Zulip Chat Archive

Stream: new members

Topic: fin 0 → false


view this post on Zulip Heather Macbeth (Jan 10 2021 at 19:49):

What's the right way to prove this? (I give a method which seems like the wrong way.)

import data.equiv.fin

example : fin 0  false := equiv.false_equiv_empty.symm  fin_zero_equiv

view this post on Zulip Kenny Lau (Jan 10 2021 at 19:50):

fin.elim0

view this post on Zulip Yakov Pechersky (Jan 10 2021 at 19:54):

What's the guidance in using fin.elim0 over fin_zero_elim?

view this post on Zulip Eric Wieser (Jan 10 2021 at 19:59):

One eliminates to things other than false, right?

view this post on Zulip Eric Wieser (Jan 10 2021 at 20:00):

docs#fin.elim0, docs#fin_zero_elim

view this post on Zulip Eric Wieser (Jan 10 2021 at 20:02):

Ah, one is mathlib the other is core, they're otherwise identical

view this post on Zulip Yakov Pechersky (Jan 10 2021 at 20:03):

Then I don't understand the docstring

view this post on Zulip Eric Wieser (Jan 10 2021 at 20:08):

#2055 gives some history

view this post on Zulip Yakov Pechersky (Jan 10 2021 at 20:09):

Ah, backward compat


Last updated: May 15 2021 at 02:11 UTC