finset_map — Mathlib

English

If f and g commute as embeddings, then the induced Finset maps commute: map f and map g satisfy commute.

Русский

Если f и g коммютируют (как вложения), то соответствующие Finset-образы коммутируют.

LaTeX

$$$\mathrm{Commute}(\mathrm{map}\ f, \mathrm{map}\ g)$$$

Lean4

theorem _root_.Function.Commute.finset_map {f g : α ↪ α} (h : Function.Commute f g) :
    Function.Commute (map f) (map g) :=
  Function.Semiconj.finset_map h

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