bind_ret — Mathlib

English

Naturality of map with join: map f (join S) = join (map (map f) S).

Русский

Естественность отображения по отображению и объединению: map f (join S) = join (map (map f) S).

LaTeX

$$$\\operatorname{map} f (\\mathrm{join}\\; S) = \\mathrm{join}(\\operatorname{map}(\\mathrm{map} f)\\; S)$$$

Lean4

@[simp]
theorem bind_ret (f : α → β) : ∀ s, bind s (ret ∘ f) = map f s
  | ⟨a, s⟩ => by simp [bind, map, map_comp, ret]

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