pmap_nil

Mathlib.Data.Vector.Defs

URI: https://scilib.ai/kg/mathlib#List.Vector.pmap_nil

English

pmap of nil is nil: nil.pmap f hp = nil.

Русский

pmap от пустого вектора равен пустому вектору: nil.pmap f hp = nil.

LaTeX

$$@[simp]\\npmap_nil (f : (a : \\alpha) → p a → β) (hp : ∀ x ∈ nil.toList, p x) : nil.pmap f hp = nil$$

Lean4

@[simp]
theorem pmap_nil (f : (a : α) → p a → β) (hp : ∀ x ∈ nil.toList, p x) : nil.pmap f hp = nil :=
  rfl

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

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

Разделы

Аффилиация

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