instSMulFilter — Mathlib

English

The action of α on Filter β is given by f ↦ map (a • ·) f.

Русский

Действие α на Filter β задаётся отображением f ↦ map (a • ·) f.

LaTeX

$$$ a \cdot f = \mathrm{map}(x \mapsto a \cdot x) f$$$

Lean4

/-- `a • f` is the map of `f` under `a •` in scope `Pointwise`. -/
@[to_additive /-- `a +ᵥ f` is the map of `f` under `a +ᵥ` in scope `Pointwise`. -/
    ]
protected def instSMulFilter : SMul α (Filter β) :=
  ⟨fun a => map (a • ·)⟩

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