image — Mathlib

English

If G is generated by x, then the image subpresheaf G.image f is generated by the family f.app(X_i)(x_i).

Русский

Если G порожден через x, то образная подпредпрешеф G.image f порождается семейством $f_{X_i}(x_i)$.

LaTeX

$$$G\text{ isGeneratedBy } x \Rightarrow (G.image\ f)\text{ isGeneratedBy } (\lambda i. f.app (X_i) (x_i))$$$

Lean4

theorem image {F' : Cᵒᵖ ⥤ Type w} (f : F ⟶ F') : (G.image f).IsGeneratedBy (fun i ↦ f.app _ (x i)) := by
  simp only [isGeneratedBy_iff, ← h.iSup_eq, image_iSup, ofSection_image]

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