length_pos_of_prod_lt_one — Mathlib

English

If L.prod < 1 in a preorder monoid M, then L is nonempty.

Русский

Если L.prod < 1 в предикатном моноиде M, то список непуст.

LaTeX

$$$ L.prod < 1 \Rightarrow 0 < L.length $$$

Lean4

/-- A list with product less than one must have positive length. -/
@[to_additive /-- A list with negative sum must have positive length. -/
    ]
theorem length_pos_of_prod_lt_one [Preorder M] (L : List M) (h : L.prod < 1) : 0 < L.length :=
  length_pos_of_prod_ne_one L h.ne

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