wcovBy_congr_right — Mathlib

English

If a and b are antisymmetrically related, then c ⩿ a iff c ⩿ b.

Русский

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

LaTeX

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

Lean4

theorem wcovBy_congr_right (hab : AntisymmRel (· ≤ ·) a b) : c ⩿ a ↔ c ⩿ b :=
  ⟨fun h => h.trans_antisymm_rel hab, fun h => h.trans_antisymm_rel hab.symm⟩

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