English
If every element of a nonempty list l of a commutative ordered monoid M is strictly greater than 1, then the product l.prod is strictly greater than 1.
Русский
Если каждый элемент непустого списка l в коммутативном упорядоченном моноиде M строго больше 1, то произведение l.prod строго больше 1.
LaTeX
$$$\\forall l:\\, \\text{List } M,\\ (\\forall x\\in l,\\ 1 < x) \\Rightarrow l \\neq \\varnothing \\Rightarrow 1 < l.prod.$$
Lean4
@[to_additive sum_pos]
theorem one_lt_prod_of_one_lt [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] :
∀ l : List M, (∀ x ∈ l, (1 : M) < x) → l ≠ [] → 1 < l.prod
| [], _, h => (h rfl).elim
| [b], h, _ => by simpa using h
| a :: b :: l, hl₁, _ => by
simp only [forall_eq_or_imp, List.mem_cons] at hl₁
rw [List.prod_cons]
apply one_lt_mul_of_lt_of_le' hl₁.1
apply le_of_lt ((b :: l).one_lt_prod_of_one_lt _ (l.cons_ne_nil b))
grind
