Mathlib Map

Theorems · Theorem · order theory

Set.injOn_of_injective

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

Around this declaration

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

Function.Injective.injOn · cited by 280Injective.injOninfinite_not_isOfFinAddOrder · cited by 2infinite_not_isOfFinAddOr…Function.HasFiniteSupport.comp_of_injective · cited by 2HasFiniteSupport.comp_of_…DivisorChain.element_of_chain_eq_pow_second_of_chain · cited by 1DivisorChain.element_of_c…Subgroup.map_iInf · cited by 1Subgroup.map_iInfFunction.HasFiniteMulSupport.comp_of_injective · cited by 1HasFiniteMulSupport.comp_…infinite_not_isOfFinOrder · cited by 1infinite_not_isOfFinOrdergroupHomology.H1CoresCoinfOfTrivial_exact · cited by 1groupHomology.H1CoresCoin…AddSubgroup.map_iInf · cited by 1AddSubgroup.map_iInfSubsemigroup.map_iInf · cited by 0Subsemigroup.map_iInfNonUnitalSubring.map_iInf · cited by 0NonUnitalSubring.map_iInfAddRightCancelMonoid.infinite_not_isOfFinAddOrder · cited by 0AddRightCancelMonoid.infi…Submonoid.map_iInf · cited by 0Submonoid.map_iInfFintype.existsUnique_notMem_image_of_injective_of_card_eq_add_one · cited by 0Fintype.existsUnique_notM…NonUnitalStarAlgebra.map_iInf · cited by 0NonUnitalStarAlgebra.map_…Set · cited by 53352SetSet.InjOn · cited by 543Set.InjOnSet.injOn_of_injectiveCITED BYCITES

Cites2

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

Cited by28

Results whose statement or proof uses this declaration.