prod_diff_prod — Mathlib

English

The difference of two product sets decomposes as a union of two independent products.

Русский

Разность двух произведений распадается на объединение двух независимых произведений.

LaTeX

$$$ s \times t \setminus s_1 \times t_1 = s \times (t \setminus t_1) \cup (s \setminus s_1) \times t $$$

Lean4

theorem prod_diff_prod : s ×ˢ t \ s₁ ×ˢ t₁ = s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t := by grind

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