fromSpecStalkOfMem_compHom — Mathlib

English

For f: X.PartialMap Y and g: Y ⟶ Z, the identity (f.compHom g).fromSpecStalkOfMem (x) hx equals f.fromSpecStalkOfMem hx followed by g.

Русский

Для f: X.PartialMap Y и g: Y ⟶ Z выполняется: (f.compHom g).fromSpecStalkOfMem (x) hx = f.fromSpecStalkOfMem hx ≫ g.

LaTeX

$$$$ (f.compHom g).fromSpecStalkOfMem (x := x) hx = f.fromSpecStalkOfMem hx \\;\\gg g $$$$

Lean4

@[simp]
theorem fromSpecStalkOfMem_compHom (f : X.PartialMap Y) (g : Y ⟶ Z) (x) (hx) :
    (f.compHom g).fromSpecStalkOfMem (x := x) hx = f.fromSpecStalkOfMem hx ≫ g := by simp [fromSpecStalkOfMem]

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