mul_congr_left — Mathlib

English

If x1 ≈ x2 and x1, x2, y are numeric, then x1 * y ≈ x2 * y.

Русский

Если x1 ≈ x2 и x1, x2, y — числовые игры, то x1·y ≈ x2·y.

LaTeX

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

Lean4

theorem mul_congr_left (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hy : y.Numeric) (he : x₁ ≈ x₂) : x₁ * y ≈ x₂ * y :=
  equiv_iff_game_eq.2 <| (P24 hx₁ hx₂ hy).1 he

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