covBy_congr_right — Mathlib

English

If a and b are equivalent under ≤, then CovBy with c from the right is preserved: c ⋖ a iff c ⋖ b.

Русский

Если a и b эквивалентны относительно ≤, тогда c ⋖ a эквивалентно c ⋖ b.

LaTeX

$$$ (\\text{AntisymmRel}(\\le)\\ a\\ b) \\Rightarrow (\\,c \\,⋖\\, a \\iff c \\,⋖\\, b) $$$

Lean4

theorem covBy_congr_right (hab : AntisymmRel (· ≤ ·) a b) : c ⋖ a ↔ c ⋖ b :=
  ⟨fun h => h.trans_antisymmRel hab, fun h => h.trans_antisymmRel hab.symm⟩

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