card_support_mul_le — Mathlib

English

The support of a product is bounded by the product of the supports: card((p q).support) ≤ card(p.support) · card(q.support).

Русский

Опора произведения ограничена произведением опор: card((p q).support) ≤ card(p.support) · card(q.support).

LaTeX

$$card((p * q).support) ≤ card(p.support) * card(q.support)$$

Lean4

theorem card_support_mul_le : #(p * q).support ≤ #p.support * #q.support := by
  calc
    #(p * q).support
    _ = #(p.toFinsupp * q.toFinsupp).support := by rw [← support_toFinsupp, toFinsupp_mul]
    _ ≤ #(p.toFinsupp.support + q.toFinsupp.support) :=
      (Finset.card_le_card (AddMonoidAlgebra.support_mul p.toFinsupp q.toFinsupp))
    _ ≤ #p.support * #q.support := Finset.card_image₂_le ..

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