compRel_congr_left — Mathlib

English

If AntisymmRel (≤) a b holds, then CompRel (≤) a c is equivalent to CompRel (≤) b c for any c.

Русский

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

LaTeX

$$AntisymmRel(\le) a b \Rightarrow Iff(CompRel(\le) a c)(CompRel(\le) b c)$$

Lean4

theorem compRel_congr_left (h : AntisymmRel (· ≤ ·) a b) : CompRel (· ≤ ·) a c ↔ CompRel (· ≤ ·) b c :=
  h.compRel_congr .rfl

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