Theorems · Definition · order theory
SetRel.id
{α : Type u_1} → SetRel α αThe identity relation.
- Defined in
- Mathlib.Data.Rel
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.ofPredproof · cited by 6,101
- SetRelstatement · cited by 581
Cited by39
Results whose statement or proof uses this declaration.
- uniformContinuous_of_constproof · cited by 4
- refl_le_uniformitystatement · cited by 4
- DiscreteUniformity.eq_principal_setRelIdstatement · cited by 3
- SetRel.id_subsetstatement and proof · cited by 3
- IsUniformEmbedding.discreteUniformityproof · cited by 3
- UniformSpace.Core.reflstatement · cited by 2
- UniformSpace.uniformSpace_eq_botstatement · cited by 1
- UniformSpace.Core.mk.injstatement and proof · cited by 1
- UniformSpace.Core.mk.noConfusionstatement and proof · cited by 1
- SetRel.preimage_idstatement · cited by 1
- comap_uniformity_of_spaced_outstatement · cited by 1
- SetRel.comp_idstatement · cited by 1