germ_res_apply — Mathlib

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]

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