Theorems · Theorem · combinatorics

List.Vector.map_pmap

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

Defined in

Mathlib.Data.Vector.MapLemmas

Cited by

0 results in Mathlib

Foundations

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