mem_map_iff — Mathlib

English

Let v be a vector of length n, f a function from α to β, and b a element of β. Then b belongs to the list (v.map f).toList if and only if there exists a ∈ α with a ∈ v.toList and f a = b.

Русский

Пусть v — вектор длины n, f: α → β — отображение, и b ∈ β. Тогда b принадлежит списку (v.map f).toList тогда и только тогда, когда существует a ∈ α такого, что a ∈ v.toList и f a = b.

LaTeX

$$$b \in (v.map f).toList \iff \exists a : \alpha, a \in v.toList \land f a = b$$$

Lean4

theorem mem_map_iff (b : β) (v : Vector α n) (f : α → β) : b ∈ (v.map f).toList ↔ ∃ a : α, a ∈ v.toList ∧ f a = b := by
  rw [Vector.toList_map, List.mem_map]

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