one_prod — Mathlib

English

The left unit acts as the identity for the pointwise product with any filter l on β: (1 : Filter α) ×ˢ l = map (1, ·) l.

Русский

Левая единица служит тождественным элементом для точечного произведения с любым фильтром l на β: (1 : Filter α) ×ˢ l = map (1, ·) l.

LaTeX

$$$(1 : Filter \\alpha) \\timesˢ l = \\mathrm{map}( (1,\\cdot) )\, l$$$

Lean4

@[to_additive (attr := simp) zero_prod]
theorem one_prod {l : Filter β} : (1 : Filter α) ×ˢ l = map (1, ·) l :=
  pure_prod

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