admissible_of_one_lt_sumInv_aux — Mathlib

English

If pqr is a sorted 3-term list with 1 < sumInv(pqr), then Admissible of the multiset {p,q,r}.

Русский

Если pqr упорядочен как три элемента и 1 < sumInv(pqr), то {p,q,r} допустимо.

LaTeX

$$$\operatorname{Admissible}(\operatorname{ofList}(p,q,r))$ under LT condition$$

Lean4

theorem admissible_of_one_lt_sumInv_aux :
    ∀ {pqr : List ℕ+} (_ : pqr.Sorted (· ≤ ·)) (_ : pqr.length = 3) (_ : 1 < sumInv pqr), Admissible pqr
  | [p, q, r], hs, _, H =>
    by
    obtain ⟨⟨hpq, -⟩, hqr⟩ : (p ≤ q ∧ p ≤ r) ∧ q ≤ r := by simpa using hs
    exact admissible_of_one_lt_sumInv_aux' hpq hqr H

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