le_generate

Mathlib.CategoryTheory.Sites.Sieves

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sieve.le_generate

English

The generated sieve is the least sieve containing the given presieve.

Русский

Порождаемый свит — минимальный свит, содержащий данный пресейв.

LaTeX

$$le_generate$$

Lean4

theorem le_generate (R : Presieve X) : R ≤ generate R :=
  giGenerate.gc.le_u_l R

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

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

Разделы

Аффилиация

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