pure_smul — Mathlib

English

The product of a pure filter at a with any filter g is the pushforward of g along a, i.e., (pure a) • g = map (a • ·) g.

Русский

Произведение чистого фильтра на a и фильтра g эквивалентно образу переноса фильтра g по действию a: (pure a) • g = map (a • ·) g.

LaTeX

$$$(\text{pure } a) \cdot g = g \mapsto (a \cdot \;)$$

Lean4

@[to_additive (attr := simp)]
theorem pure_smul : (pure a : Filter α) • g = g.map (a • ·) :=
  map₂_pure_left

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