empty_inter

Mathlib.Data.Set.Basic

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

English

For any set a, ∅ ∩ a = ∅.

Русский

Для любого множества A выполняется ∅ ∩ A = ∅.

LaTeX

$$$\emptyset \cap a = \emptyset$$$

Lean4

@[simp]
theorem empty_inter (a : Set α) : ∅ ∩ a = ∅ :=
  ext fun _ => iff_of_eq (false_and _)

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

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

Разделы

Аффилиация

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