trans — Mathlib

English

If P3(x1, x2, y1, y2) and P3(x2, x3, y1, y2), then P3(x1, x3, y1, y2).

Русский

Если P3(x1, x2, y1, y2) и P3(x2, x3, y1, y2), то P3(x1, x3, y1, y2).

LaTeX

$$$$ \mathrm{P3}(x_1,x_2,y_1,y_2) \wedge \mathrm{P3}(x_2,x_3,y_1,y_2) \rightarrow \mathrm{P3}(x_1,x_3,y_1,y_2). $$$$

Lean4

theorem trans (h₁ : P3 x₁ x₂ y₁ y₂) (h₂ : P3 x₂ x₃ y₁ y₂) : P3 x₁ x₃ y₁ y₂ :=
  by
  rw [P3] at h₁ h₂
  rw [P3, ← add_lt_add_iff_left (⟦x₂ * y₁⟧ + ⟦x₂ * y₂⟧)]
  convert add_lt_add h₁ h₂ using 1 <;> abel

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