RFC: `Std.Trans`

Proposal

I propose adding the following class to src/Init/Core.lean:

/-- `Trans r` means that the binary relation `r` is transitive, that is, `r a b → r b c → r a c`.  -/
class Trans (α : Sort _) (r : α → α → Prop) : Prop where
  /-- A transitive relation satisfies `r a b → r b c → r a c`. -/
  trans : ∀ a b c, r a b → r b c → r a c

This would join the existing docs#Std.Refl, docs#Std.Symm, docs#Std.Trichotomous, etc.

There is the existing docs#Trans but it takes in 3 relations and is geared towards calc. Additionally, Trans r r r isn't a Prop because it has max 1 in its universe.

Community Feedback

#lean4 > RFC: `Std.Trans`

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start with the proposal in src/Init/Core.lean and compare it with the existing Std.Refl, Std.Symm, and Std.Trichotomous declarations linked in the issue. Read the linked Zulip discussion and the existing Trans documentation to determine whether the proposed class and naming are accepted; done means the RFC has a clear decision and implementation scope.