Theorems · Theorem · combinatorics

List.Vector.mem_map_iff

∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (b : β) (v : List.Vector α n) (f : α → β),
  b ∈ (List.Vector.map f v).toList ↔ ∃ a ∈ v.toList, f a = b

Defined in

Mathlib.Data.Vector.Mem

Cited by

1 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound