mulEnergy_self_pos

Mathlib.Combinatorics.Additive.Energy

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

English

If s is nonempty, then Eₘ[s] > 0.

Русский

Если s не пусто, энергия Eₘ[s] положительна.

LaTeX

$$$ s \\neq \\emptyset \\Rightarrow 0 < E_m[s] $$$

Lean4

@[to_additive]
theorem mulEnergy_self_pos (hs : s.Nonempty) : 0 < Eₘ[s] :=
  mulEnergy_pos hs hs

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

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

Разделы

Аффилиация

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