mulEnergy_eq_card_filter — Mathlib

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])

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