pure_vsub — Mathlib

English

For any a and any filter g on β, the vsub of the principal filter at a with g is g translated by a.

Русский

Для любого элемента a и любого фильтра g на β разность f -ᵥ g, где f — чистый фильтр в точке a, равна переносу g по a.

LaTeX

$$$ (\text{pure } a) -ᵥ g = g.map (x \mapsto a -ᵥ x)$$$

Lean4

@[simp]
theorem pure_vsub : (pure a : Filter β) -ᵥ g = g.map (a -ᵥ ·) :=
  map₂_pure_left

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