mk_mul_le — Mathlib

English

For any subsets s,t ⊆ M with a multiplication, the set s t = { x y : x ∈ s, y ∈ t } has cardinality at most |s|·|t|.

Русский

Для подмножеств s, t ⊆ M с умножением, множество произведений s t = { x y : x ∈ s, y ∈ t } не крупнее чем произведение кардиналов |s|·|t|.

LaTeX

$$$$ |s t| \\le |s| \\cdot |t| $$$$

Lean4

@[to_additive]
theorem _root_.Cardinal.mk_mul_le : #(s * t) ≤ #s * #t := by rw [← image2_mul]; exact Cardinal.mk_image2_le

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