le_mulEnergy_self

Mathlib.Combinatorics.Additive.Energy

URI: https://scilib.ai/kg/mathlib#Finset.le_mulEnergy_self

English

The square of the size of s is at most the energy of s with itself: |s|^2 ≤ Eₘ[s].

Русский

Квадрат размера множества s не превосходит энергии Eₘ[s]: |s|^2 ≤ Eₘ[s].

LaTeX

$$$ |s|^2 \\le E_m[s] $$$

Lean4

@[to_additive]
theorem le_mulEnergy_self : #s ^ 2 ≤ Eₘ[s] :=
  sq #s ▸ le_mulEnergy

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

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

Разделы

Аффилиация

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