English
A specialized form of germ_res applied to a concrete category structure; expresses the equality after applying F.map to s.
Русский
Специализированная форма germ_res, примененная к конкретной структуре категории; выражает равенство после применения F.map к s.
LaTeX
$$$F.germ U x hx (F.map i.op s) = F.germ V x (i.le hx) s$$$
Lean4
theorem germ_res_apply (F : X.Presheaf C) {U V : Opens X} (i : U ⟶ V) (x : X) (hx : x ∈ U) [ConcreteCategory C FC] (s) :
F.germ U x hx (F.map i.op s) = F.germ V x (i.le hx) s := by rw [← ConcreteCategory.comp_apply, germ_res]