Theorems · Inductive type · logic and foundations
Relation.EqvGen
{α : Type u_1} → (α → α → Prop) → α → α → PropEqvGen r: equivalence closure of r.
- Defined in
- Mathlib.Logic.Relation
- Cited by
- 49 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by56
Results whose statement or proof uses this declaration.
- JordanHolderLattice.Isoproof · cited by 13
- Relation.EqvGen.setoidproof · cited by 10
- Equivalence.eqvGen_iffstatement and proof · cited by 9
- Quot.eqstatement · cited by 9
- Quot.eqvGen_soundstatement and proof · cited by 9
- Quot.eqvGen_exactstatement · cited by 6
- CategoryTheory.Limits.Types.FilteredColimit.eqvGen_colimitTypeRel_of_relstatement and proof · cited by 6
- Relation.EqvGen.eqvGen_lestatement and proof · cited by 6
- Relation.EqvGen.monostatement and proof · cited by 5
- Setoid.eqvGen_eqproof · cited by 4
- Relation.EqvGen.eqvGen_monostatement and proof · cited by 4
- CategoryTheory.Quotient.functor_homRel_eq_compClosure_eqvGenstatement · cited by 4