mulEnergy_eq_zero_iff

Mathlib.Combinatorics.Additive.Energy

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

← MathLib Explorer

English

E_m[s,t] = 0 iff s = ∅ or t = ∅.

Русский

E_m[s,t] = 0 тогда и только тогда, когда s = ∅ или t = ∅.

LaTeX

$$$ E_m[s,t] = 0 \\iff s = \\emptyset \\lor t = \\emptyset $$$

Lean4

@[to_additive (attr := simp)]
theorem mulEnergy_eq_zero_iff : Eₘ[s, t] = 0 ↔ s = ∅ ∨ t = ∅ := by
  simp [← (Nat.zero_le _).not_lt_iff_eq', imp_iff_or_not, or_comm]

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

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

Разделы

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

Аффилиация

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