inter_prod

Mathlib.Data.Set.Prod

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

English

The product of the empty set with any t is empty: ∅ × t = ∅.

Русский

Произведение пустого множества слева с любым t равно пустому множеству: ∅ × t = ∅.

LaTeX

$$$ \emptyset \times t = \emptyset $$$

Lean4

theorem inter_prod : (s₁ ∩ s₂) ×ˢ t = s₁ ×ˢ t ∩ s₂ ×ˢ t :=
  by
  ext ⟨x, y⟩
  simp only [← and_and_right, mem_inter_iff, mem_prod]

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

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

Разделы

Аффилиация

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