instTransLeAntisymmRel — Mathlib

English

The antisymmetric relation lifted from ≤ is compatible with the original ordering: if a ≤ b and b ≤ c in the antisymmetric sense, then a ≤ c holds in α.

Русский

Антисимметрическое отношение, порождаемое ≤, совместимо с исходным порядком: если a ≤ b и b ≤ c в антисимметрическом смысле, то a ≤ c.

LaTeX

$$$\\forall a,b,c \\in \\alpha,\\ a \\le b \\to AntisymmRel(\\le)\\,b\\,c \\to a \\le c$$$

Lean4

instance : @Trans α α α (· ≤ ·) (AntisymmRel (· ≤ ·)) (· ≤ ·) where trans := le_of_le_of_antisymmRel

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