mulEnergy_mono_left

Mathlib.Combinatorics.Additive.Energy

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

English

If s1 ⊆ s2, then Eₘ[s1,t] ≤ Eₘ[s2,t].

Русский

Если s1 ⊆ s2, тогда Eₘ[s1,t] ≤ Eₘ[s2,t].

LaTeX

$$$ E_m[s_1,t] \\le E_m[s_2,t] \\quad\\text{whenever } s_1 \\subseteq s_2 $$$

Lean4

@[to_additive]
theorem mulEnergy_mono_left (hs : s₁ ⊆ s₂) : Eₘ[s₁, t] ≤ Eₘ[s₂, t] :=
  mulEnergy_mono hs Subset.rfl

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

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

Разделы

Аффилиация

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