div_pure — Mathlib

English

Dividing by a pure filter corresponds to composing with a division by the fixed element: f / pure b = f.map (· / b).

Русский

Деление на чистый фильтр эквивалентно отображению через деление на фиксированное b: f / pure b = f.map( x \\mapsto x / b ).

LaTeX

$$$f / \\text{pure } b = f.map(\\cdot / b).$$$

Lean4

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

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