inter_nil'

Mathlib.Data.List.Lattice

URI: https://scilib.ai/kg/mathlib#List.inter_nil'

English

For any list l, the intersection with the empty list is empty: l ∩ [] = [].

Русский

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

LaTeX

$$$\\\\forall {\\\\alpha} [\\\\mathrm{DecidableEq} \\\\alpha] (l : List \\\\alpha), l \\\\cap [] = []$$$

Lean4

@[simp, grind =]
theorem inter_nil' (l : List α) : l ∩ [] = [] := by induction l with grind

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

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

Разделы

Аффилиация

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