mulEnergy_mono

Mathlib.Combinatorics.Additive.Energy

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

English

If s1 ⊆ s2 and t1 ⊆ t2, then Eₘ[s1,t1] ≤ Eₘ[s2,t2].

Русский

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

LaTeX

$$$ E_m[s_1,t_1] \\le E_m[s_2,t_2] \\quad\\text{whenever } s_1 \\subseteq s_2 \\text{ and } t_1 \\subseteq t_2 $$$

Lean4

@[to_additive (attr := gcongr)]
theorem mulEnergy_mono (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : Eₘ[s₁, t₁] ≤ Eₘ[s₂, t₂] := by unfold mulEnergy; gcongr

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

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

Разделы

Аффилиация

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