map_pure_prod — Mathlib

English

For f : α → β → γ and a ∈ α and B a filter on β, map (uncurry f) (pure a ×ˢ B) equals map (f a) B.

Русский

Пусть f : α → β → γ, a ∈ α и B — фильтр на β. Тогда map (uncurry f) (pure a × B) = map (f a) B.

LaTeX

$$$ \\operatorname{map}(\\operatorname{uncurry} f)\\bigl(\\mathrm{pure}(a) \\times\\! B\\bigr) = \\operatorname{map}(f(a))\\, B $$$

Lean4

theorem map_pure_prod (f : α → β → γ) (a : α) (B : Filter β) : map (Function.uncurry f) (pure a ×ˢ B) = map (f a) B :=
  by rw [Filter.pure_prod]; rfl

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