Eliminate #X = 0

Stream: new members

[Pedro Minicz]

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]

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

[Alex J. Best]

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

[Reid Barton]

ahh it's phrased in terms of ≠

[Kevin Buzzard]

heh, ne_zero_iff_nonempty

[Kevin Buzzard]

looks like someone missed a trick

[Kevin Buzzard]

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

[Pedro Minicz]

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.

[Mario Carneiro]

it can't though

[Mario Carneiro]

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