compRel_congr_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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