one_lt_sumInv — Mathlib

English

For any multiset pqr of naturals, if pqr is admissible then 1 < sumInv pqr.

Русский

Для любого мультинабора pqr натуральных чисел, если pqr допустим, то 1 < sumInv pqr.

LaTeX

$$$\forall pqr: \text{Multiset} \mathbb{N}^+\; (\operatorname{Admissible}(pqr) \Rightarrow 1 < \operatorname{sumInv}(pqr))$$$

Lean4

theorem one_lt_sumInv {pqr : Multiset ℕ+} : Admissible pqr → 1 < sumInv pqr :=
  by
  rw [Admissible]
  rintro (⟨p', q', H⟩ | ⟨n, H⟩ | H | H | H)
  · rw [← H, A', sumInv_pqr, add_assoc]
    simp only [lt_add_iff_pos_right, PNat.one_coe, inv_one, Nat.cast_one]
    apply add_pos <;> simp only [PNat.pos, Nat.cast_pos, inv_pos]
  · rw [← H, D', sumInv_pqr]
    norm_num
  all_goals
    rw [← H, E', sumInv_pqr]
    norm_num

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