prod_pure — Mathlib

English

For f : Filter α and b ∈ β the product with pure b equals the image of f under the shift by b: f ×ˢ pure b = map (λ a ↦ (a,b)) f.

Русский

Для фильтра f на α и фиксированного b ∈ β выполняется: f ×ˢ pure b = map (λ a. (a,b)) f.

LaTeX

$$$ f \\times\\! \\mathrm{pure}(b) = \\operatorname{map}(\\lambda a. (a,b))\\, f $$$

Lean4

@[simp]
theorem prod_pure {b : β} : f ×ˢ pure b = map (fun a => (a, b)) f := by rw [prod_eq, seq_pure, map_map]; rfl

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