lt_of_antisymmRel_of_lt — Mathlib

English

Let α be a preorder. If a is related to b by antisymmetric relation and b < c, then a < c.

Русский

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

LaTeX

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

Lean4

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

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