mulEnergy_self_pos_iff

Mathlib.Combinatorics.Additive.Energy

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

English

0 < E_m[s] iff s is nonempty.

Русский

0 < E_m[s] тогда и только тогда, когда s непусто.

LaTeX

$$$0 < E_m[s] \\iff s.Nonempty$$$

Lean4

@[to_additive]
theorem mulEnergy_self_pos_iff : 0 < Eₘ[s] ↔ s.Nonempty := by rw [mulEnergy_pos_iff, and_self_iff]

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

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

Разделы

Аффилиация

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