filter_map — Mathlib

English

If f and g commute, then their Filter.map versions commute as well.

Русский

Если функции f и g коммютируют, то их отображения через Filter.map также коммютируют.

LaTeX

$$$ \text{Function.Commute}(f,g) \Rightarrow \text{Function.Commute}(\mathrm{Filter.map} f, \mathrm{Filter.map} g) $$$

Lean4

theorem _root_.Function.Commute.filter_map {f g : α → α} (h : Function.Commute f g) :
    Function.Commute (map f) (map g) :=
  h.semiconj.filter_map

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