wcovBy_congr_left — Mathlib

English

If a and b are antisymmetrically related (in the left argument), then a ⩿ c iff b ⩿ c.

Русский

Если a и b антисимметрично связаны слева, то a ⩿ c эквивалентно b ⩿ c.

LaTeX

$$$AntisymmRel (\\\\le) a b \\\\Rightarrow (a \\\\mathrel{\\\\trianglelefteq} c \\\iff b \\\\mathrel{\\\\trianglelefteq} c).$$$

Lean4

theorem wcovBy_congr_left (hab : AntisymmRel (· ≤ ·) a b) : a ⩿ c ↔ b ⩿ c :=
  ⟨hab.symm.trans_wcovBy, hab.trans_wcovBy⟩

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