image_iSup — Mathlib

English

For a family of subpresheaves Gi of F, the image under f distributes over arbitrary suprema: image of the supremum equals the supremum of the images.

Русский

Для семейства подпрешеф Gi над F отображение под действием f распределяется по произвольному супремуму: образ верхнего предела равен супремуму образов.

LaTeX

$$$ (\\bigsqcup_i G_i).\\mathrm{image}\\,f = \\bigsqcup_i (G_i).\\mathrm{image}\\,f $$$

Lean4

@[simp]
theorem image_iSup {ι : Type*} (G : ι → Subpresheaf F) (f : F ⟶ F') : (⨆ i, G i).image f = ⨆ i, (G i).image f := by
  aesop

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