le_prod_of_mem

Mathlib.Algebra.Order.BigOperators.Group.Multiset

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

← MathLib Explorer

English

If a ∈ m, then a ≤ m.prod in a canonically ordered monoid.

Русский

Если a ∈ m, то a ≤ m.prod в канонически упорядоченном монаде.

LaTeX

$$$ a \in m \Rightarrow a \le m.prod $$$

Lean4

@[to_additive]
theorem le_prod_of_mem (ha : a ∈ m) : a ≤ m.prod :=
  by
  obtain ⟨t, rfl⟩ := exists_cons_of_mem ha
  rw [prod_cons]
  exact _root_.le_mul_right (le_refl a)

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

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

Разделы

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

Аффилиация

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