map_comp — Mathlib

English

Mapping under a composition equals composing mappings: map(g ∘ f) H = map g (map f H).

Русский

Отображение через композицию равно последовательному отображению: map(g ∘ f) H = map g (map f H).

LaTeX

$$$ (H.map (g \circ f)) = (H.map f).map g $$$

Lean4

theorem map_comp {U : Type*} {G'' : SimpleGraph U} (H : G.Subgraph) (f : G →g G') (g : G' →g G'') :
    H.map (g.comp f) = (H.map f).map g := by ext <;> simp [Subgraph.map]

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