English
E_m[s,t] equals the cardinality of a filtered product set: E_m[s,t] = #({x ∈ ((s × t) × (s × t)) | x.1.1 * x.1.2 = x.2.1 * x.2.2}).
Русский
E_m[s,t] равно кардиналу отфильтрованного множества: E_m[s,t] = #({x ∈ ((s × t) × (s × t)) | x.1.1 * x.1.2 = x.2.1 * x.2.2}).
LaTeX
$$$ E_m[s,t] = \\#\\{x \\in ((s \\times t) \\times (s \\times t)) \\mid x.1.1 \\cdot x.1.2 = x.2.1 \\cdot x.2.2\\}\\ $$$
Lean4
@[to_additive]
theorem mulEnergy_eq_card_filter (s t : Finset α) :
Eₘ[s, t] = #({x ∈ ((s ×ˢ t) ×ˢ s ×ˢ t) | x.1.1 * x.1.2 = x.2.1 * x.2.2}) :=
card_equiv (.prodProdProdComm _ _ _ _) (by simp [and_and_and_comm])