Theorems · Theorem · combinatorics

List.Vector.map_map

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (xs : List.Vector α n) (f₁ : β → γ) (f₂ : α → β),
  List.Vector.map f₁ (List.Vector.map f₂ xs) = List.Vector.map (fun x => f₁ (f₂ x)) xs

Defined in

Mathlib.Data.Vector.MapLemmas

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext