ofSection_image — Mathlib

English

The image of ofSection x under f equals ofSection (f.app x).

Русский

Образ ofSection x под действием f равен ofSection (f.app x).

LaTeX

$$$ (\\mathrm{ofSection}\\ x).\\mathrm{image}\\ f = \\mathrm{ofSection} (f.\\mathrm{app}\\ _\\ x) $$$

Lean4

@[simp]
theorem ofSection_image {F' : Cᵒᵖ ⥤ Type w} (f : F ⟶ F') : (ofSection x).image f = ofSection (f.app _ x) :=
  by
  apply le_antisymm
  · rw [image_le_iff, ofSection_le_iff, preimage_obj, Set.mem_preimage]
    exact ⟨𝟙 X, by simp⟩
  · simp only [ofSection_le_iff, image_obj, Set.mem_image]
    exact ⟨x, mem_ofSection_obj x, rfl⟩

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