P1_of_lt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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