prod_le_pow_card — Mathlib

English

Let l be a finite list of elements of M and n ∈ M with every element x ∈ l satisfying n ≤ x. Then n raised to the power |l| is a lower bound for the product l.prod:

Русский

Пусть l — конечный список элементов M и n ∈ M так, что для каждого x ∈ l выполняется n ≤ x. Тогда n^{|l|} является нижней границей произведения l.prod.

LaTeX

$$$\\forall l:\\, \\text{List } M,\\ n\\in M,\\ (\\forall x\\in l,\\ n \\le x) \\Rightarrow n^{|l|} \\le l.prod.$$

Lean4

@[to_additive sum_le_card_nsmul]
theorem prod_le_pow_card [Preorder M] [MulRightMono M] [MulLeftMono M] (l : List M) (n : M) (h : ∀ x ∈ l, x ≤ n) :
    l.prod ≤ n ^ l.length := by simpa only [map_id', map_const', prod_replicate] using prod_le_prod' h

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