le_congr — Mathlib

English

If a ≤ b and c ≤ d are related by antisymmetry, 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 le_congr (h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : AntisymmRel (· ≤ ·) c d) : a ≤ c ↔ b ≤ d
    where
  mp h := (h₁.symm.trans_le h).trans_antisymmRel h₂
  mpr h := (h₁.trans_le h).trans_antisymmRel h₂.symm

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