prod_union

Mathlib.Data.Set.Prod

URI: https://scilib.ai/kg/mathlib#Set.prod_union

English

Distributes over union in the second factor: s × (t1 ∪ t2) = (s × t1) ∪ (s × t2).

Русский

Произведение с объединением во втором множителе: s × (t1 ∪ t2) = (s × t1) ∪ (s × t2).

LaTeX

$$$ s \times (t_1 \cup t_2) = (s \times t_1) \cup (s \times t_2) $$$

Lean4

@[simp]
theorem prod_union : s ×ˢ (t₁ ∪ t₂) = s ×ˢ t₁ ∪ s ×ˢ t₂ :=
  by
  ext ⟨x, y⟩
  simp [and_or_left]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru