Theorems · Theorem · logic and foundations
Cardinal.not_injective_limitation_set
∀ {α : Type u} (g : Ordinal.{u} → α), ¬Set.InjOn g (Set.Iio (SuccOrder.succ (Cardinal.mk α)).ord)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.Elemproof · cited by 7,166
- Cardinalstatement and proof · cited by 2,598
- Ordinalstatement and proof · cited by 1,688
- Set.Iiostatement and proof · cited by 1,166
- Cardinal.mkstatement and proof · cited by 942
- Cardinal.liftproof · cited by 583
- Set.InjOnstatement and proof · cited by 543
- Cardinal.ordstatement and proof · cited by 266
- not_le_of_gtproof · cited by 97
- Cardinal.lift_leproof · cited by 78
- Cardinal.lift_liftproof · cited by 53
- Order.lt_succproof · cited by 45
Cited by1
Results whose statement or proof uses this declaration.
- OrdinalApprox.exists_lfpApprox_eq_lfpApproxproof · cited by 2