Theorems · Theorem · order theory
Set.injOn_iff_injective
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.InjOn f s ↔ Function.Injective (s.domRestrict f)- Defined in
- Mathlib.Data.Set.Restrict
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.Elemstatement and proof · cited by 7,166
- Set.InjOnstatement and proof · cited by 543
- Set.domRestrictstatement and proof · cited by 383
Cited by20
Results whose statement or proof uses this declaration.
- Set.InjOn.injectiveproof · cited by 6
- Set.MapsTo.countable_of_injOnproof · cited by 5
- Set.MapsTo.restrict_injproof · cited by 4
- Set.not_injOn_infinite_finite_imageproof · cited by 4
- OrdinalApprox.exists_lfpApprox_eq_lfpApproxproof · cited by 2
- IsTranscendenceBasis.of_isAlgebraic_adjoin_insert_sdiffproof · cited by 2
- LinearIndepOn.image_of_compproof · cited by 2
- LinearIndepOn.injOnproof · cited by 2
- IsClosed.measurableSet_image_of_continuousOn_injOnproof · cited by 1
- AlgebraicIndependent.image_of_compproof · cited by 1
- Set.exists_injOn_iff_injectiveproof · cited by 1
- Orthonormal.exists_orthonormalBasis_extension_of_card_eqproof · cited by 1