Theorems · Theorem · combinatorics

List.Vector.comp_traverse

∀ {n : ℕ} {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative G] {α β γ : Type u}
  (f : β → F γ) (g : α → G β) (x : List.Vector α n),
  List.Vector.traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x =
    Functor.Comp.mk (List.Vector.traverse f <$> List.Vector.traverse g x)

Defined in

Mathlib.Data.Vector.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

ApplicativeApplicativeLawfulApplicative