ofSection_le — Mathlib

English

Let G be a subpresheaf of F generated by a family x = (x_i) indexed by ι through objects X(i). Then each generator x_i lies in G at X(i). In particular, G contains all the sections x_i.

Русский

Пусть G — подпрешеф F, порожденный семейством x = (x_i) по индексному множеству ι и через объекты X(i). Тогда каждый x_i принадлежит G в точке X(i). В частности, x_i ∈ G(X_i) для всех i.

LaTeX

$$$G\text{ isGeneratedBy } x \Rightarrow \forall i:\iota,\ x_i \in G(X_i)$$$

Lean4

theorem ofSection_le (i : ι) : ofSection (x i) ≤ G :=
  by
  rw [← h.iSup_eq]
  exact le_iSup (fun i ↦ ofSection (x i)) i

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