Theorems · Definition · logic and foundations
Equiv.ofInjective
{α : Sort u_3} → {β : Type u_4} → (f : α → β) → Function.Injective f → α ≃ ↑(Set.range f)If f : α → β is an injective function, then domain α is equivalent to the range of f.
- Defined in
- Mathlib.Logic.Equiv.Set
- Cited by
- 64 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement · cited by 8,337
- Set.Elemstatement · cited by 7,166
- Set.rangestatement · cited by 4,705
- Function.invFunproof · cited by 60
- Function.leftInverse_invFunproof · cited by 13
- Equiv.ofLeftInverseproof · cited by 4
Cited by88
Results whose statement or proof uses this declaration.
- Finite.of_injectiveproof · cited by 32
- Module.Basis.reindexRangeproof · cited by 16
- LinearIndependent.cardinal_lift_le_rankproof · cited by 16
- Topology.IsEmbedding.toHomeomorphproof · cited by 16
- small_of_injectiveproof · cited by 15
- MvPolynomial.killComplproof · cited by 15
- Cardinal.mk_range_eq_of_injectiveproof · cited by 14
- Equiv.ofInjective_applystatement and proof · cited by 10
- Equiv.ofInjective_symm_applystatement and proof · cited by 8
- Equiv.apply_ofInjective_symmstatement and proof · cited by 8
- LieAlgebra.Extension.toKerproof · cited by 8
- IsTranscendenceBasis.lift_cardinalMk_eq_trdegproof · cited by 7