lt_add_of_lt — Mathlib

English

If v_p(q) < v_p(r1) and v_p(q) < v_p(r2), then v_p(q) < v_p(r1 + r2).

Русский

Если v_p(q) меньше, чем v_p(r1) и v_p(r2), то v_p(q) меньше, чем v_p(r1 + r2).

LaTeX

$$$ v_p(q) < v_p(r_1) \\land v_p(q) < v_p(r_2) \\Rightarrow v_p(q) < v_p(r_1 + r_2) $$$

Lean4

theorem lt_add_of_lt {q r₁ r₂ : ℚ} (hqr : r₁ + r₂ ≠ 0) (hval₁ : padicValRat p q < padicValRat p r₁)
    (hval₂ : padicValRat p q < padicValRat p r₂) : padicValRat p q < padicValRat p (r₁ + r₂) :=
  lt_of_lt_of_le (lt_min hval₁ hval₂) (padicValRat.min_le_padicValRat_add hqr)

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