map_def — Mathlib

English

The Functor instance for Filter coincides with Filter.map, i.e., applying map to a filter is the same as the existing map operation.

Русский

Инстанс функторов для Filter совпадает с операцией Filter.map: применение map к фильтру эквивалентно существующему отображению.

LaTeX

$$$ m \lhd f = \operatorname{map}(m,f) $$$

Lean4

@[simp]
theorem map_def {α β} (m : α → β) (f : Filter α) : m <$> f = map m f :=
  rfl

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