subcanonical — Mathlib

English

The regular topology on any preregular category is subcanonical.

Русский

Регулярная топология на любой прегеормально-регулярной категории субканонична.

LaTeX

$$instance subcanonical [Preregular C] : (regularTopology C).Subcanonical$$

Lean4

/-- The regular topology on any preregular category is subcanonical. -/
instance subcanonical [Preregular C] : (regularTopology C).Subcanonical :=
  GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ isSheaf_yoneda_obj

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