Zulip Chat Archive

Stream: new members

Topic: Eliminate #X = 0


view this post on Zulip Pedro Minicz (Aug 12 2020 at 16:43):

Couldn't find a say to eliminate x : X into false given #X = 0. library_search/suggest aren't helping much, have I missed something in the docs?

import set_theory.cardinal

open_locale cardinal

example {X : Type} (h : #X = 0) (x : X) : false :=
begin
  apply pempty.elim,
  let κ := # X,
  -- How do I eliminate `x`?
  sorry
end

view this post on Zulip Reid Barton (Aug 12 2020 at 16:48):

Looks like it may be missing. See the proof of mk_emptyc_iff

view this post on Zulip Alex J. Best (Aug 12 2020 at 16:48):

open cardinal
example {X : Type} (h : #X = 0) (x : X) : false :=
   ne_zero_iff_nonempty.mpr (nonempty.intro x) h

view this post on Zulip Reid Barton (Aug 12 2020 at 16:49):

ahh it's phrased in terms of ≠

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 17:21):

heh, ne_zero_iff_nonempty

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 17:21):

looks like someone missed a trick

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 17:21):

Oh! The issue is that nobody knows the canonical way to say a type is empty! I vote for X -> false FWIW

view this post on Zulip Pedro Minicz (Aug 12 2020 at 17:28):

Why not rename pempty to false and use it everywhere? :thinking:

It would seem a bit weird initially but, if Lean can infer the sort correctly most cases, it should work great.

view this post on Zulip Mario Carneiro (Aug 12 2020 at 17:47):

it can't though

view this post on Zulip Mario Carneiro (Aug 12 2020 at 17:48):

the reason why none of the p* definitions are used by default is because it makes universe inference less reliable than it normally is


Last updated: May 06 2021 at 21:09 UTC