sUnion_prod_const — Mathlib

English

Union with a family of products distributes: ⋃₀ C × t = ⋃₀ (f''t)'' C.

Русский

Объединение с семейством произведений распадается на объединение произведений.

LaTeX

$$$\bigcup_0 C \times t = \bigcup_{s \in C} (s \times t)$$$

Lean4

theorem sUnion_prod_const {C : Set (Set α)} {t : Set β} : ⋃₀ C ×ˢ t = ⋃₀ ((fun s : Set α => s ×ˢ t) '' C) := by
  simp only [sUnion_eq_biUnion, iUnion₂_prod_const, biUnion_image]

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