Theorems · Theorem · logic and foundations

Cardinal.mk_equiv_eq_arrow_of_lift_eq

∀ {α : Type u} {β' : Type v} [Infinite α],
  Cardinal.lift.{v, u} (Cardinal.mk α) = Cardinal.lift.{u, v} (Cardinal.mk β') →
    Cardinal.mk (α ≃ β') = Cardinal.mk (α → β')

Defined in

Mathlib.SetTheory.Cardinal.Arithmetic

Cited by

2 results in Mathlib

Foundations

Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Infinite