admissible_of_one_lt_sumInv — Mathlib

English

For any p,q,r ∈ ℕ+, if 1 < sumInv{p,q,r}, then {p,q,r} is Admissible.

Русский

Для любых p,q,r ∈ ℕ+, если 1 < sumInv{p,q,r}, то {p,q,r} допустимо.

LaTeX

$$$\forall p,q,r \in \mathbb{N}_{+},\ 1 < \mathrm{sumInv}\{p,q,r\} \Rightarrow \operatorname{Admissible}\{p,q,r\}$$$

Lean4

theorem admissible_of_one_lt_sumInv {p q r : ℕ+} (H : 1 < sumInv { p, q, r }) : Admissible { p, q, r } :=
  by
  simp only [Admissible]
  let S := sort ((· ≤ ·) : ℕ+ → ℕ+ → Prop) { p, q, r }
  have hS : S.Sorted (· ≤ ·) := sort_sorted _ _
  have hpqr : ({ p, q, r } : Multiset ℕ+) = S := (sort_eq LE.le { p, q, r }).symm
  rw [hpqr]
  rw [hpqr] at H
  apply admissible_of_one_lt_sumInv_aux hS _ H
  simp only [S, insert_eq_cons, length_sort, card_cons, card_singleton]

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