Theorems · Theorem · order theory
trans
∀ {α : Sort u_1} {r : α → α → Prop} {a b c : α} [IsTrans α r], r a b → r b c → r a c- Defined in
- Mathlib.Order.Defs.Unbundled
- Cited by
- 111 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 1 definitions · uses no axioms
- Assumes
- IsTrans
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.
- IsTransstatement and proof · cited by 157
- IsTrans.transproof · cited by 22
Cited by111
Results whose statement or proof uses this declaration.
- PrincipalSeg.mem_range_of_relproof · cited by 24
- Polynomial.degree_map_eq_of_leadingCoeff_ne_zeroproof · cited by 9
- trans_ofproof · cited by 9
- Polynomial.eval₂_eq_sum_rangeproof · cited by 9
- Ideal.comap_isMaximal_of_surjectiveproof · cited by 8
- Filter.IsBounded.isCobounded_flipproof · cited by 8
- Fin.liftFun_iff_succproof · cited by 6
- Directed.finset_leproof · cited by 6
- Relation.EqvGen.eqvGen_leproof · cited by 6
- MvPolynomial.mem_supportedproof · cited by 4
- Int.rel_of_forall_rel_succ_of_ltproof · cited by 4
- Concept.mem_extent_of_rel_extentproof · cited by 4