Theorems · Definition · order theory
Setoid.sigmaQuotientEquivOfLe
{α : Type u_1} → {r s : Setoid α} → r ≤ s → (q : Quotient s) × Quotient (Setoid.comap Subtype.val r) ≃ Quotient rGiven two equivalence relations with r ≤ s, a bijection between the sum of the quotients by
r on each equivalence class by s and the quotient by r.
- Defined in
- Mathlib.Data.Setoid.Basic
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Equivstatement · cited by 8,337
- Set.preimagestatement and proof · cited by 4,946
- Equiv.symmproof · cited by 3,681
- Equiv.transproof · cited by 337
- Equiv.sigmaFiberEquivproof · cited by 18
- Setoid.comapstatement · cited by 16
- Equiv.sigmaCongrRightproof · cited by 12
- Equiv.subtypeQuotientEquivQuotientSubtypeproof · cited by 4
Cited by2
Results whose statement or proof uses this declaration.
- AddAction.equivAddSubgroupOrbitsproof · cited by 0
- MulAction.equivSubgroupOrbitsproof · cited by 0