empty_inter

Mathlib.Data.Finset.Lattice.Lemmas

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

English

For every finite set S, the intersection with the empty set is empty: ∅ ∩ S = ∅.

Русский

Для любого конечного множества S пересечение с пустым множеством равно пустому множеству: ∅ ∩ S = ∅.

LaTeX

$$$\\emptyset \\cap S = \\emptyset$$$

Lean4

@[simp]
theorem empty_inter (s : Finset α) : ∅ ∩ s = ∅ :=
  ext fun _ => mem_inter.trans <| by simp

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

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

Разделы

Аффилиация

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