lt_congr — Mathlib

English

If a ≼ b and c ≼ d, then a < c iff b < d.

Русский

Если a ≼ b и c ≼ d, то a < c эквивалентно b < d.

LaTeX

$$$\\forall a,b,c,d \\in α,\\ AntisymmRel(≤) a b \\to AntisymmRel(≤) c d \\to (a < c) \\leftrightarrow (b < d)$$$

Lean4

theorem lt_congr (h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : AntisymmRel (· ≤ ·) c d) : a < c ↔ b < d
    where
  mp h := (h₁.symm.trans_lt h).trans_antisymmRel h₂
  mpr h := (h₁.trans_lt h).trans_antisymmRel h₂.symm

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