antisymmRel_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 (AntisymmRel(≤) a c) \\leftrightarrow (AntisymmRel(≤) b d)$$$

Lean4

theorem antisymmRel_congr (h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : AntisymmRel (· ≤ ·) c d) :
    AntisymmRel (· ≤ ·) a c ↔ AntisymmRel (· ≤ ·) b d :=
  rel_congr h₁ h₂

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