mul_pure — Mathlib

English

The product of a filter f with a pure filter at b equals the image of f under multiplication by b: f * pure b = f.map (· * b).

Русский

Произведение фильтра f на чистый фильтр pure b равно образу f под умножением на b: f * pure b = f.map (· * b).

LaTeX

$$$$ f * pure b = f.map (\cdot \; * \; b). $$$$

Lean4

@[to_additive (attr := simp)]
theorem mul_pure : f * pure b = f.map (· * b) :=
  map₂_pure_right

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