Theorems · Definition
Function.FactorsThrough
{α : Sort u_1} → {β : Sort u_2} → {γ : Sort u_3} → (α → γ) → (α → β) → Propg factors through f : f a = f b → g a = g b
- Defined in
- Mathlib.Logic.Function.Basic
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by22
Results whose statement or proof uses this declaration.
- Topology.IsQuotientMap.liftstatement and proof · cited by 6
- Function.FactorsThrough.extend_applystatement and proof · cited by 6
- dependsOn_iff_factorsThroughstatement and proof · cited by 5
- Function.Injective.factorsThroughstatement · cited by 4
- Measurable.factorsThroughstatement · cited by 3
- Topology.IsQuotientMap.liftEquivstatement and proof · cited by 3
- MeasureTheory.StronglyMeasurable.factorsThroughstatement · cited by 2
- Function.factorsThrough_iffstatement and proof · cited by 2
- Topology.IsQuotientMap.lift_compstatement and proof · cited by 2
- Pairwise.disjoint_extend_botstatement and proof · cited by 1
- Topology.IsQuotientMap.lift_applystatement and proof · cited by 1
- factorsThrough_of_pullbackConditionstatement · cited by 1