commutative_map

Mathlib.Control.Basic

URI: https://scilib.ai/kg/mathlib#CommApplicative.commutative_map

Lean4

theorem commutative_map {m : Type u → Type v} [h : Applicative m] [CommApplicative m] {α β γ} (a : m α) (b : m β)
    {f : α → β → γ} : f <$> a <*> b = flip f <$> b <*> a :=
  calc
    f <$> a <*> b = (fun p : α × β => f p.1 p.2) <$> (Prod.mk <$> a <*> b) := by
      simp only [map_seq, map_map, Function.comp_def]
    _ = (fun b a => f a b) <$> b <*> a :=
      by
      rw [@CommApplicative.commutative_prod m h]
      simp [map_seq, map_map]
      rfl

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru