le_canonical

Mathlib.CategoryTheory.Sites.Canonical

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.le_canonical

English

If a Grothendieck topology J is Subcanonical, then J is contained in the canonical topology on C.

Русский

Если топология Гротендекса J субкононична, то она содержится в канонической топологии на C.

LaTeX

$$$J \\le \\mathrm{canonicalTopology}(C)$$$

Lean4

theorem le_canonical (J : GrothendieckTopology C) [Subcanonical J] : J ≤ canonicalTopology C :=
  Subcanonical.le_canonical

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

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

Разделы

Аффилиация

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