Theorems · Definition · order theory
Setoid.kerLift
{α : Type u_1} → {β : Type u_2} → (f : α → β) → Quotient (Setoid.ker f) → βGiven a function f, lift it to the quotient by its kernel.
- Defined in
- Mathlib.Data.Setoid.Basic
- Cited by
- 9 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.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setoid.kerstatement · cited by 43
Cited by11
Results whose statement or proof uses this declaration.
- Topology.IsEmbedding.isStrictMap_iffproof · cited by 6
- Setoid.kerLift_injectivestatement and proof · cited by 2
- Setoid.quotientKerEquivOfRightInverseproof · cited by 2
- Topology.isStrictMap_iff_isEmbedding_kerLiftstatement and proof · cited by 1
- Setoid.range_kerLift_eq_rangestatement · cited by 0
- Function.RightInverse.homeomorph_applystatement · cited by 0
- Setoid.kerLift_mkstatement · cited by 0
- Topology.IsQuotientMap.homeomorph_applystatement · cited by 0
- Setoid.quotientKerEquivOfRightInverse_applystatement · cited by 0
- Setoid.lift_injective_iff_ker_eq_of_leproof · cited by 0
- Setoid.quotientKerEquivRangeKerLiftstatement and proof · cited by 0