nil_product

Mathlib.Data.List.ProdSigma

URI: https://scilib.ai/kg/mathlib#List.nil_product

English

The sprod with a nil list on the left yields the empty list, i.e., nil ×ˢ l = [] for any l.

Русский

Произведение со списком nil слева даёт пустой список: nil ×ˢ l = [].

LaTeX

$$$\forall l:\\ List β, \\ (\\mathbf{nil} : List α) ×ˢ l = []$$$

Lean4

@[simp]
theorem nil_product (l : List β) : (@nil α) ×ˢ l = [] :=
  rfl

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

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

Разделы

Аффилиация

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