Theorems · Theorem

Traversable.traverse_map

∀ {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {F : Type u → Type u} [inst_2 : Applicative F]
  [LawfulApplicative F] {α β γ : Type u} (f : β → F γ) (g : α → β) (x : t α), traverse f (g <$> x) = traverse (f ∘ g) x

Defined in

Mathlib.Control.Traversable.Lemmas

Cited by

6 results in Mathlib

Foundations

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

Assumes

TraversableLawfulTraversableApplicativeLawfulApplicative