Theorems · Definition
Equiv.subtypeEquivProp
{α : Sort u_1} → {p q : α → Prop} → p = q → Subtype p ≃ Subtype qIf two predicates are equal, then the corresponding subtypes are equivalent.
- Defined in
- Mathlib.Logic.Equiv.Basic
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement · cited by 8,337
- Equiv.reflproof · cited by 274
- Equiv.subtypeEquivproof · cited by 32
Cited by19
Results whose statement or proof uses this declaration.
- Equiv.setCongrproof · cited by 13
- PrincipalSeg.subrelIsoproof · cited by 6
- Ideal.associatesNonZeroDivisorsEquivIsPrincipalproof · cited by 5
- WeierstrassCurve.Affine.nonsingularPointEquivproof · cited by 4
- WeierstrassCurve.Affine.pointEquivproof · cited by 4
- WeierstrassCurve.Affine.pointEquivSubtypeproof · cited by 4
- AlgebraicGeometry.affineOpensRestrictproof · cited by 3
- Homeomorph.ofEqSubtypesproof · cited by 2
- AlgebraicGeometry.opensRestrictproof · cited by 2
- PadicInt.continuousAddCharEquiv_of_norm_mulproof · cited by 2
- EisensteinSeries.gammaSetDivGcdSigmaEquivproof · cited by 2
- PrincipalSeg.apply_subrelIsoproof · cited by 1