lt_of_lt_of_antisymmRel — Mathlib

English

Let α be a preorder. If a is strictly less than b and b is related to c via the antisymmetric relation generated from ≤, then a is strictly less than c.

Русский

Пусть α — множество с предобразным частичным порядком. Если a < b и b связан с c через антисимметрическое отношение, порождаемое ≤, то a < c.

LaTeX

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

Lean4

theorem lt_of_lt_of_antisymmRel (h₁ : a < b) (h₂ : AntisymmRel (· ≤ ·) b c) : a < c :=
  h₁.trans_le h₂.le

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