## Stream: new members

### Topic: Eliminate #X = 0

#### 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


#### Reid Barton (Aug 12 2020 at 16:48):

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

#### 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


#### Reid Barton (Aug 12 2020 at 16:49):

ahh it's phrased in terms of ≠

#### Kevin Buzzard (Aug 12 2020 at 17:21):

heh, ne_zero_iff_nonempty

#### Kevin Buzzard (Aug 12 2020 at 17:21):

looks like someone missed a trick

#### 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

#### 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.

it can't though

#### 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