Theorems · Definition · logic and foundations
Equiv.setCongr
{α : Type u_3} → {s t : Set α} → s = t → ↑s ≃ ↑tThe subtypes corresponding to equal sets are equivalent.
- Defined in
- Mathlib.Logic.Equiv.Set
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Quot.sound
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.
- Setstatement and proof · cited by 53,352
- Equivstatement · cited by 8,337
- Set.Elemstatement · cited by 7,166
- Equiv.subtypeEquivPropproof · cited by 6
Cited by57
Results whose statement or proof uses this declaration.
- LinearEquiv.ofEqproof · cited by 32
- Homeomorph.setCongrproof · cited by 29
- NumberField.Ideal.primesOverSpanEquivMonicFactorsModproof · cited by 10
- MulEquiv.subgroupCongrproof · cited by 10
- OrderIso.setCongrproof · cited by 10
- Equiv.Finset.unionproof · cited by 9
- LinearMap.trace_conj'proof · cited by 8
- WithVal.valueGroupEquivproof · cited by 8
- finSumEquivOfFinsetproof · cited by 7
- finEquivZPowersproof · cited by 6
- Equiv.Set.insertproof · cited by 6
- AddEquiv.addSubgroupCongrproof · cited by 6