compRel_congr — Mathlib

English

If AntisymmRel (≤) a b and AntisymmRel (≤) c d hold, then CompRel (≤) a c is equivalent to CompRel (≤) b d.

Русский

Если AntisymmRel (≤) a b и AntisymmRel (≤) c d выполняются, то CompRel (≤) a c эквивалентно CompRel (≤) b d.

LaTeX

$$AntisymmRel(\le) a b \rightarrow AntisymmRel(\le) c d \rightarrow Iff(CompRel(\le) a c)(CompRel(\le) b d)$$

Lean4

theorem compRel_congr (h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : AntisymmRel (· ≤ ·) c d) :
    CompRel (· ≤ ·) a c ↔ CompRel (· ≤ ·) b d
    where
  mp h := (h₁.symm.trans_compRel h).trans_antisymmRel h₂
  mpr h := (h₁.trans_compRel h).trans_antisymmRel h₂.symm

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