notMem_map_zero — Mathlib

English

For any f: α → β and any vector v of length 0, b ∉ (v.map f).toList for every b ∈ β.

Русский

Для любой функции f: α → β и вектора v нулевой длины, для любого b ∈ β выполняется b не принадлежит (v.map f).toList.

LaTeX

$$$b \notin (v.map f).toList$$$

Lean4

theorem notMem_map_zero (b : β) (v : Vector α 0) (f : α → β) : b ∉ (v.map f).toList := by
  simpa only [Vector.eq_nil v, Vector.map_nil, Vector.toList_nil] using List.not_mem_nil

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