mulEnergy_pos

Mathlib.Combinatorics.Additive.Energy

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

English

If s and t are nonempty, then Eₘ[s,t] > 0.

Русский

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

LaTeX

$$$ s \\neq \\emptyset \\land t \\neq \\emptyset \\Rightarrow 0 < E_m[s,t] $$$

Lean4

@[to_additive]
theorem mulEnergy_pos (hs : s.Nonempty) (ht : t.Nonempty) : 0 < Eₘ[s, t] :=
  (mul_pos hs.card_pos ht.card_pos).trans_le le_mulEnergy

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

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

Разделы

Аффилиация

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