Theorems · Theorem · combinatorics

List.Vector.pmap_map

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (xs : List.Vector α n) {p : β → Prop} (f₁ : (b : β) → p b → γ)
  (f₂ : α → β) (H : ∀ x ∈ (List.Vector.map f₂ xs).toList, p x),
  List.Vector.pmap f₁ (List.Vector.map f₂ xs) H = List.Vector.pmap (fun x hx => f₁ (f₂ x) hx) xs ⋯

Defined in

Mathlib.Data.Vector.MapLemmas

Cited by

0 results in Mathlib

Foundations

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