instIsTransSubsequent — Mathlib

English

The relation Subsequent is transitive: if x is subsequent to y and y is subsequent to z, then x is subsequent to z.

Русский

Отношение Subsequent транзитивно: если x последовательно следует за y, а y — за z, то x последовательно следует за z.

LaTeX

$$$\forall x,y,z:\ \text{SetTheory.PGame},\ x\!\subsequent\!y \wedge y\!\subsequent\!z \Rightarrow x\!\subsequent\!z.$$$

Lean4

instance : IsTrans _ Subsequent :=
  inferInstanceAs <| IsTrans _ (TransGen _)

Похожие утверждения