Theorems · Theorem
Function.Bijective.of_comp_iff
∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α},
Function.Bijective g → (Function.Bijective (f ∘ g) ↔ Function.Bijective f)- Defined in
- Mathlib.Logic.Function.Basic
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 8 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.
- Function.Bijectivestatement and proof · cited by 863
- Function.Bijective.surjectiveproof · cited by 114
- Function.Injective.of_comp_iff'proof · cited by 8
- Function.Surjective.of_comp_iffproof · cited by 7
Cited by22
Results whose statement or proof uses this declaration.
- CategoryTheory.Adjunction.map_comp_bijective_iffproof · cited by 3
- CategoryTheory.GrothendieckTopology.W_inverseImage_whiskeringLeftproof · cited by 2
- HomotopicalAlgebra.bijective_rightHomotopyClassToHomproof · cited by 2
- EquivLike.bijective_compproof · cited by 2
- Algebra.TensorProduct.includeLeft_bijectiveproof · cited by 2
- LinearMap.linearProjOfIsCompl_comp_bijective_of_exactproof · cited by 1
- CategoryTheory.Functor.CoconeTypes.IsColimit.iff_bijectiveproof · cited by 1
- CategoryTheory.GrothendieckTopology.W.whiskerLeftproof · cited by 1
- CategoryTheory.Presheaf.nonempty_isLimit_mapCone_iffproof · cited by 1
- CategoryTheory.Presieve.isSheafFor_pullback_iffproof · cited by 1
- CategoryTheory.Functor.IsRepresentedBy.iff_isIso_uliftYonedaEquivproof · cited by 1
- DirectSum.toBaseChange_injectiveproof · cited by 1