mul_congr_right — Mathlib

English

If x is numeric and y1 ≈ y2 with y1, y2 numeric, then x*y1 ≈ x*y2.

Русский

Если x числовая, а y1 ≈ y2 и y1, y2 числовые, то x·y1 ≈ x·y2.

LaTeX

$$$$ \forall x\,y_1\,y_2\; (x.Numeric \land y_1.Numeric \land y_2.Numeric \land y_1 \approx y_2) \Rightarrow x \cdot y_1 \approx x \cdot y_2. $$$$

Lean4

theorem mul_congr_right (hx : x.Numeric) (hy₁ : y₁.Numeric) (hy₂ : y₂.Numeric) (he : y₁ ≈ y₂) : x * y₁ ≈ x * y₂ :=
  .trans (mul_comm_equiv _ _) <| .trans (mul_congr_left hy₁ hy₂ hx he) (mul_comm_equiv _ _)

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