isSeparating_empty_of_thin

Mathlib.CategoryTheory.Generator.Basic

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

English

If the category is thin, then the empty set is separating.

Русский

Если категория тонкая, то пустое множество является разделяющим.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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