Theorems · Theorem · logic and foundations
Cardinal.mk_le_of_injective
∀ {α β : Type u} {f : α → β}, Function.Injective f → Cardinal.mk α ≤ Cardinal.mk β- Defined in
- Mathlib.SetTheory.Cardinal.Order
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Cardinalstatement · cited by 2,598
- Cardinal.mkstatement · cited by 942
Cited by12
Results whose statement or proof uses this declaration.
- Cardinal.mk_realproof · cited by 11
- HasCardinalLT.of_injectiveproof · cited by 9
- Cardinal.mk_finsupp_lift_of_infiniteproof · cited by 6
- Cardinal.mk_finset_of_infiniteproof · cited by 2
- WType.cardinalMk_le_of_le'proof · cited by 2
- Metric.packingNumber_two_mul_le_externalCoveringNumberproof · cited by 2
- IsTranscendenceBasis.lift_cardinalMk_eq_max_liftproof · cited by 1
- Cardinal.mk_bounded_subsetproof · cited by 1
- OreLocalization.cardinalMkproof · cited by 1
- Cardinal.mk_freeAddGroupproof · cited by 0
- Cardinal.mk_subset_mk_lt_cofproof · cited by 0
- Cardinal.mk_freeGroupproof · cited by 0