congr_app — Mathlib

English

A variant of congruence for morphisms in presheafed spaces with a specified equality h.

Русский

Вариант конгруэнтности для морфизмов прешефдов пространства с заданным равенством h.

LaTeX

$$$\forall X,Y, \alpha = \beta \Rightarrow \alpha.c.app(U) = \beta.c.app(U) \circ X.presheaf.map(\text{eqToHom}(⋯))$$$

Lean4

theorem congr_app {X Y : PresheafedSpace C} {α β : X ⟶ Y} (h : α = β) (U) :
    α.c.app U = β.c.app U ≫ X.presheaf.map (eqToHom (by subst h; rfl)) :=
  by
  subst h
  simp

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