Theorems · Theorem · logic and foundations

Cardinal.mk_surjective_eq_arrow_of_lift_le

∀ {α : Type u} {β' : Type v} [Infinite α],
  Cardinal.lift.{u, v} (Cardinal.mk β') ≤ Cardinal.lift.{v, u} (Cardinal.mk α) →
    Cardinal.mk ↑{f | Function.Surjective f} = Cardinal.mk (α → β')

Defined in: Mathlib.SetTheory.Cardinal.Arithmetic
Cited by: 1 results in Mathlib
Foundations: Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Infinite

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites20

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Equivproof · cited by 8,337
Set.Elemstatement and proof · cited by 7,166
Set.ofPredstatement and proof · cited by 6,101
Equiv.symmproof · cited by 3,681
Cardinalstatement and proof · cited by 2,598
Cardinal.mkstatement and proof · cited by 942
Cardinal.liftstatement and proof · cited by 583
LE.le.antisymmproof · cited by 507
Infinitestatement and proof · cited by 352
Equiv.apply_symm_applyproof · cited by 346
Equiv.right_invproof · cited by 68

Cited by1

Results whose statement or proof uses this declaration.

Cardinal.mk_surjective_eq_arrow_of_leproof · cited by 0