filter_comap — Mathlib

English

If f and g commute, then Filter.map preserves their commute: Filter.map f and Filter.map g commute.

Русский

Если 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_comap {f g : α → α} (h : Function.Commute f g) :
    Function.Commute (comap f) (comap g) :=
  h.semiconj.filter_comap

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