product_disjUnion — Mathlib

English

If t is disjoint from t', then s × (t.disjUnion t' ht) equals the disjoint union of (s × t) and (s × t') with a suitable witness.

Русский

Если t раздельно от t', то s × (t.disjUnion t' ht) равно объединению (s × t) и (s × t') с нужным доказательством.

LaTeX

$$$s \\timesˢ (t.disjUnion t' ht) = (s \\timesˢ t) \\\\disjUnion (s \\timesˢ t') (disjoint_product.mpr (Or.inr ht))$$$

Lean4

@[simp]
theorem product_disjUnion (ht : Disjoint t t') :
    s ×ˢ t.disjUnion t' ht = (s ×ˢ t).disjUnion (s ×ˢ t') (disjoint_product.mpr <| Or.inr ht) :=
  eq_of_veq <| Multiset.product_add _ _ _

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