map_nil — Mathlib

English

For any f : α → β, map f nil = nil. The image of the empty vector under a coordinatewise map remains empty.

Русский

Для каждого f : α → β отображение пустого вектора координатным отображением дает пустой вектор: map f nil = nil.

LaTeX

$$$\\forall f:\\alpha\\to\\beta,\\ map\\ f\\ nil = nil$$$

Lean4

/-- A `nil` vector maps to a `nil` vector. -/
@[simp]
theorem map_nil (f : α → β) : map f nil = nil :=
  rfl

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