single_le_prod

Mathlib.Algebra.Order.BigOperators.Group.Multiset

URI: https://scilib.ai/kg/mathlib#Multiset.single_le_prod

← MathLib Explorer

English

In an ordered monoid, every element x in a multiset s satisfies x ≤ s.prod.

Русский

В упорядоченном монаде каждое x ∈ s удовлетворяет x ≤ s.prod.

LaTeX

$$$ \forall x \in s, x \le s.prod $$$

Lean4

@[to_additive]
theorem single_le_prod [IsOrderedMonoid α] : (∀ x ∈ s, (1 : α) ≤ x) → ∀ x ∈ s, x ≤ s.prod :=
  Quotient.inductionOn s fun l hl x hx => by simpa using List.single_le_prod hl x hx

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru