isDetector_unop_iff

Mathlib.CategoryTheory.Generator.Basic

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

← MathLib Explorer

English

IsDetector(unop G) is equivalent to IsCodetector G.

Русский

IsDetector(unop G) эквивалентно IsCodetector G.

LaTeX

$$$$\text{IsDetector}(\mathrm{unop}\,G) \iff \text{IsCodetector}(G).$$$$

Lean4

theorem isDetector_unop_iff (G : Cᵒᵖ) : IsDetector (unop G) ↔ IsCodetector G := by
  rw [IsDetector, IsCodetector, ← isDetecting_unop_iff, Set.singleton_unop]

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

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

Разделы

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

Аффилиация

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