le_mulEnergy — Mathlib

English

The product of the cardinalities of s and t is a lower bound for the energy: |s| · |t| ≤ Eₘ[s,t].

Русский

Произведение кардиналов s и t является нижней границей энергии: |s| · |t| ≤ Eₘ[s,t].

LaTeX

$$$ |s| \\cdot |t| \\le E_m[s,t] $$$

Lean4

@[to_additive]
theorem le_mulEnergy : #s * #t ≤ Eₘ[s, t] := by
  rw [← card_product]
  exact card_le_card_of_injOn (fun x => ((x.1, x.1), x.2, x.2)) (by simp [Set.MapsTo]) (by simp)

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