prod_empty

Mathlib.Data.Set.Prod

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

English

For any s ⊆ α, s × ∅ = ∅.

Русский

Для любого s ⊆ α, s × ∅ = ∅.

LaTeX

$$$ s \times \emptyset = \emptyset $$$

Lean4

@[simp]
theorem prod_empty : s ×ˢ (∅ : Set β) = ∅ := by
  ext
  exact iff_of_eq (and_false _)

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

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

Разделы

Аффилиация

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