Library ▹ Essentials ▹ Relations
Definition 1.4.13.  Let S be a set, ≺ be a relation on S. We define:
≺ is transitive  :⇔  ∀ s, t, u ∈ S s.t. s ≺ t and t ≺ u : s ≺ u
References.
  • https://en.wikipedia.org/wiki/Transitive_relation
  • https://mathworld.wolfram.com/Transitive.html
  • https://proofwiki.org/wiki/Definition:Transitive_Relation
  • https://ncatlab.org/nlab/show/transitive+relation
  • https://coq.inria.fr/library/Coq.Sets.Relations_1.html#Transitive
  • https://leanprover-community.github.io/mathlib_docs/init/logic.html#transitive
[View Source]