comap_comap — 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

$$$ \operatorname{map}_{\text{Filter}}(m,f) = \mathrm{map}\, m\, f $$$

Lean4

theorem comap_comap {m : γ → β} {n : β → α} : comap m (comap n f) = comap (n ∘ m) f :=
  Filter.coext fun s => by simp only [compl_mem_comap, image_image, (· ∘ ·)]

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