sections_property — Mathlib

English

If s is a section of F, then for every morphism f: j ⟶ j', the map F.map f sends s(j) to s(j').

Русский

Если s — секция F, то для каждого морфизма f: j ⟶ j' отображение F.map f отправляет s(j) в s(j').

LaTeX

$$$$ \forall j,j', f: j \to j',\ F.map f (s(j)) = s(j'). $$$$

Lean4

@[simp]
theorem sections_property {F : J ⥤ Type w} (s : (F.sections : Type _)) {j j' : J} (f : j ⟶ j') :
    F.map f (s.val j) = s.val j' :=
  s.property f

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