Cardinal.mk Type

Stream: Is there code for X?

[Eric Wieser]

Is this decidable within Lean's type theory? Do we have it?

import Mathlib


open Cardinal

theorem mk_type_le_type.{u} : lift.{u + 2} #(Type u) < #(Type (u + 1)) := sorry

[Floris van Doorn]

Yes, that is in Mathlib.

[Floris van Doorn]

It's a special case of docs#Cardinal.lift_lt_univ, I think?

[Floris van Doorn]

Oh, not quite. univ is the cardinality of Cardinal, not Type*.
However, here you go:

import Mathlib

open Cardinal

theorem mk_type_le_type.{u} : lift.{u + 2} #(Type u) < #(Type (u + 1)) := by
  refine lift_lt_univ #(Type u) |>.trans_le ?_
  simp [← mk_cardinal]
  exact Cardinal.mk_quotient_le

Let me dig up the previous discussion we had about this.

[Eric Wieser]

Thanks, I remember this coming up but loogle turned up nothing for Cardinal.mk (Type _)

[Floris van Doorn]

(my Zulip search skills fail me to find the previous discussion)