Theorems · Theorem
Function.Injective.comp_left
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {g : β → γ}, Function.Injective g → Function.Injective fun x => g ∘ xComposition by an injective function on the left is itself injective.
- Defined in
- Mathlib.Logic.Function.Basic
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Function.Injective.piMapproof · cited by 5
Cited by15
Results whose statement or proof uses this declaration.
- CategoryTheory.ofHom_epi_iff_surjectiveproof · cited by 5
- CategoryTheory.ofHom_mono_iff_injectiveproof · cited by 2
- Function.comp_eq_const_iffproof · cited by 2
- groupCohomology.mem_cocycles₁_of_comp_eq_d₀₁proof · cited by 1
- Behrend.threeAPFree_sphereproof · cited by 1
- MonoidHom.compAddChar_injective_rightproof · cited by 1
- groupCohomology.mem_cocycles₂_of_comp_eq_d₁₂proof · cited by 1
- IsDenseInducing.isUniformInducing_extendproof · cited by 1
- groupHomology.chainsMap_f_map_monoproof · cited by 0
- Function.Bijective.comp_leftproof · cited by 0
- AddChar.compAddMonoidHom_injective_rightproof · cited by 0
- IsPurelyInseparable.of_injective_comp_algebraMapproof · cited by 0