isSeparated

Mathlib.CategoryTheory.Sites.SheafOfTypes

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Presieve.IsSheaf.isSeparated

English

The same monotonicity result for IsSeparated as above, expressed with presieve isSeparated notion.

Русский

Та же монотонность для IsSeparated, выраженная через понятие IsSeparated Presieve.

LaTeX

$$$IsSeparated(J_2, P) \Rightarrow IsSeparated(J_1, P)$$$

Lean4

theorem isSeparated {P : Cᵒᵖ ⥤ Type w} (h : IsSheaf J P) : IsSeparated J P := fun _ S hS => (h S hS).isSeparatedFor

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

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

Разделы

Аффилиация

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