mul_congr — Mathlib

English

If x1 ≈ x2 and y1 ≈ y2 with all four numeric, then x1*y1 ≈ x2*y2.

Русский

Если x1 ≈ x2 и y1 ≈ y2 и все четыре числа нумеричны, то x1·y1 ≈ x2·y2.

LaTeX

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

Lean4

theorem mul_congr (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hy₁ : y₁.Numeric) (hy₂ : y₂.Numeric) (hx : x₁ ≈ x₂)
    (hy : y₁ ≈ y₂) : x₁ * y₁ ≈ x₂ * y₂ :=
  .trans (mul_congr_left hx₁ hx₂ hy₁ hx) (mul_congr_right hx₂ hy₁ hy₂ hy)

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