map_comm — Mathlib

English

The defined mapEmbedding coincides with the map for any embedding f: α ↪ β, i.e., mapEmbedding f s = map f s.

Русский

Определение mapEmbedding даёт то же отображение, что и map: для любого отображения f: α ↪ β имеет место mapEmbedding f s = map f s.

LaTeX

$$$mapEmbedding f\, s = map f\, s$$$

Lean4

theorem map_comm {β'} {f : β ↪ γ} {g : α ↪ β} {f' : α ↪ β'} {g' : β' ↪ γ} (h_comm : ∀ a, f (g a) = g' (f' a)) :
    (s.map g).map f = (s.map f').map g' := by simp_rw [map_map, Embedding.trans, Function.comp_def, h_comm]

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