Mathlib Map

Theorems · Theorem · order theory

Set.BijOn.injOn

∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.BijOn f s t → Set.InjOn f s
Defined in
Mathlib.Data.Set.Function
Cited by
42 results in Mathlib
Foundations
Depth 8 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Set.BijOn.comp · cited by 6BijOn.compSet.BijOn.inter_mapsTo · cited by 5BijOn.inter_mapsToSet.BijOn.invOn_invFunOn · cited by 5BijOn.invOn_invFunOnSet.BijOn.congr · cited by 3BijOn.congrSet.BijOn.exists_extend_of_subset · cited by 2BijOn.exists_extend_of_su…threeAPFree_image · cited by 2threeAPFree_imagethreeGPFree_image · cited by 2threeGPFree_imageSet.BijOn.bijective · cited by 2BijOn.bijectiveIsAddFreimanHom.addRothNumber_mono · cited by 2IsAddFreimanHom.addRothNu…isCorner_image · cited by 2isCorner_imageIsMulFreimanIso.symm · cited by 1IsMulFreimanIso.symmFinset.sum_preimage_of_bij · cited by 1Finset.sum_preimage_of_bijSet.BijOn.finsetCard_eq · cited by 1BijOn.finsetCard_eqSet.exists_image_eq_and_injOn · cited by 1Set.exists_image_eq_and_i…Set.BijOn.insert_iff · cited by 1BijOn.insert_iffSet · cited by 53352SetSet.InjOn · cited by 543Set.InjOnSet.BijOn · cited by 168Set.BijOnBijOn.injOnCITED BYCITES

Cites3

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.InjOnstatement · cited by 543
  • Set.BijOnstatement and proof · cited by 168

Cited by42

Results whose statement or proof uses this declaration.