pure_prod — Mathlib

English

For any a ∈ α and f : Filter β, the product of pure a with f equals the image of f under the pairing with a: pure a ×ˢ f = map (Prod.mk a) f.

Русский

Для элемента a ∈ α и фильтра f на β выполняется: чистый a ×ˢ f = map (Prod.mk a) f.

LaTeX

$$$ \\text{pure } a \\times\\! f = \\operatorname{map}(\\mathrm{Prod.mk}(a))\\, f $$$

Lean4

@[simp]
theorem pure_prod {a : α} {f : Filter β} : pure a ×ˢ f = map (Prod.mk a) f := by rw [prod_eq, map_pure, pure_seq_eq_map]

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