iSup_eq

Mathlib.CategoryTheory.Subpresheaf.Finite

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

English

If G is generated by x, then the supremum over i of ofSection(x_i) equals G.

Русский

Если G сгенерирован из x, то верхняя грань над i для x_i равна G.

LaTeX

$$$G.IsGeneratedBy\\, x \\;\u2192\\; \\bigvee_i \\text{ofSection}(x_i) = G$$$

Lean4

theorem iSup_eq : ⨆ (i : ι), ofSection (x i) = G :=
  h

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

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

Разделы

Аффилиация

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