finset_map — Mathlib

English

If f: α ↪ β, ga: α ↪ α, gb: β ↪ β satisfy f ∘ ga = gb ∘ f, then the induced Finset maps satisfy map f ∘ map ga = map gb ∘ map f.

Русский

Пусть f: α ↪ β, ga: α ↪ α, gb: β ↪ β удовлетворяют f ∘ ga = gb ∘ f. Тогда соответствующие отображения Finset удовлетворяют map f ∘ map ga = map gb ∘ map f.

LaTeX

$$$\mathrm{Semiconj}(\mathrm{map}\ f,\mathrm{map}\ ga,\mathrm{map}\ gb)$$$

Lean4

theorem _root_.Function.Semiconj.finset_map {f : α ↪ β} {ga : α ↪ α} {gb : β ↪ β} (h : Function.Semiconj f ga gb) :
    Function.Semiconj (map f) (map ga) (map gb) := fun _ => map_comm h

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