isCodetecting

Mathlib.CategoryTheory.Generator.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsCoseparating.isCodetecting

← MathLib Explorer

English

If 𝒢 is codetecting, then it is coseparating.

Русский

Если 𝒢 кодетектирует, то оно косепарирует.

LaTeX

$$$IsCodetecting(\mathcal{G}) \Rightarrow IsCoseparating(\mathcal{G})$$$

Lean4

theorem isCodetecting [Balanced C] {𝒢 : Set C} : IsCoseparating 𝒢 → IsCodetecting 𝒢 := by
  simpa only [← isDetecting_op_iff, ← isSeparating_op_iff] using IsSeparating.isDetecting

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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