isCoseparating_empty_of_thin

Mathlib.CategoryTheory.Generator.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.isCoseparating_empty_of_thin

English

If the category is thin, then IsCoseparating ∅ holds.

Русский

Если категория тонкая, то IsCoseparating(∅) выполняется.

LaTeX

$$[\text{Quiver.IsThin } C] \Rightarrow IsCoseparating(\emptyset)$$

Lean4

theorem isCoseparating_empty_of_thin [Quiver.IsThin C] : IsCoseparating (∅ : Set C) := fun _ _ _ _ _ =>
  Subsingleton.elim _ _

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

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

Разделы

Аффилиация

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