mem

Mathlib.CategoryTheory.Subpresheaf.Finite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subpresheaf.IsGeneratedBy.mem

English

If G is generated by x, then for every i we have x_i ∈ G(X_i).

Русский

Если G порожден через x, то для каждого i выполняется x_i ∈ G(X_i).

LaTeX

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

Lean4

theorem mem (i : ι) : x i ∈ G.obj (X i) := by
  rw [← ofSection_le_iff]
  exact h.ofSection_le i

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru