pow_card_le_prod — Mathlib

English

Let l be a finite list of elements of M and n ∈ M with every element x ∈ l satisfying x ≤ n. Then the product l.prod is bounded above by n^{|l|}: l.prod ≤ n^{|l|}.

Русский

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

LaTeX

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

Lean4

@[to_additive card_nsmul_le_sum]
theorem pow_card_le_prod [Preorder M] [MulRightMono M] [MulLeftMono M] (l : List M) (n : M) (h : ∀ x ∈ l, n ≤ x) :
    n ^ l.length ≤ l.prod :=
  @prod_le_pow_card Mᵒᵈ _ _ _ _ l n h

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