Theorems · Theorem · logic and foundations
Cardinal.mk_range_eq_of_injective
∀ {α : Type u} {β : Type v} {f : α → β},
Function.Injective f → Cardinal.lift.{u, v} (Cardinal.mk ↑(Set.range f)) = Cardinal.lift.{v, u} (Cardinal.mk α)- Defined in
- Mathlib.SetTheory.Cardinal.Basic
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.Elemstatement · cited by 7,166
- Set.rangestatement · cited by 4,705
- Equiv.symmproof · cited by 3,681
- Cardinalstatement · cited by 2,598
- Cardinal.mkstatement · cited by 942
- Cardinal.liftstatement · cited by 583
- Equiv.ofInjectiveproof · cited by 64
- Cardinal.lift_mk_eq'proof · cited by 21
Cited by14
Results whose statement or proof uses this declaration.
- Module.Basis.mk_eq_rankproof · cited by 10
- Cardinal.lift_mk_le_lift_mk_of_injectiveproof · cited by 10
- finrank_span_eq_cardproof · cited by 7
- rank_spanproof · cited by 6
- exists_linearIndependent_cons_of_lt_rankproof · cited by 2
- Submodule.rank_eq_spanRank_of_freeproof · cited by 2
- AlgebraicIndependent.isTranscendenceBasis_of_lift_trdeg_leproof · cited by 2
- Matrix.cRank_diagonalproof · cited by 1
- Matrix.cRank_oneproof · cited by 1
- Cardinal.extend_function_finiteproof · cited by 1
- Module.Basis.le_spanproof · cited by 1
- lift_trdeg_add_leproof · cited by 1