pow_card_le_prod — Mathlib

English

If a ≤ x for all x ∈ s in a locally finite ordered monoid, then a^{|s|} ≤ s.prod.

Русский

Если a ≤ x для всех x ∈ s в локально конечном упорядоченном моноиде, то a^{|s|} ≤ s.prod.

LaTeX

$$$ (\forall x \in s, a \le x) \Rightarrow a^{|s|} \le s.prod $$$

Lean4

@[to_additive card_nsmul_le_sum]
theorem pow_card_le_prod [MulLeftMono α] (h : ∀ x ∈ s, a ≤ x) : a ^ card s ≤ s.prod :=
  by
  rw [← Multiset.prod_replicate, ← Multiset.map_const]
  exact prod_map_le_prod _ h

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