disjUnion_product — Mathlib

English

If s is disjoint from s', then (s.disjUnion s' hs) × t equals the disjoint union of (s × t) and (s' × t) with appropriate disjointness.

Русский

Если s частичноDisjoint от s', то (s.disjUnion s' hs) × t равно объединению (s × t) и (s' × t) с соответствующим свойством непересечения.

LaTeX

$$$(s.disjUnion s' hs) \\times t = (s \\times t) \\\\disjUnion (s' \\times t) (\\\\text{Or.inl } hs)$$$

Lean4

@[simp]
theorem disjUnion_product (hs : Disjoint s s') :
    s.disjUnion s' hs ×ˢ t = (s ×ˢ t).disjUnion (s' ×ˢ t) (disjoint_product.mpr <| Or.inl hs) :=
  eq_of_veq <| Multiset.add_product _ _ _

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