isDetector_op_iff

Mathlib.CategoryTheory.Generator.Basic

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

English

IsDetector(op G) is equivalent to IsCodetector G.

Русский

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

LaTeX

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

Lean4

theorem isDetector_op_iff (G : C) : IsDetector (op G) ↔ IsCodetector G := by
  rw [IsDetector, IsCodetector, ← isDetecting_op_iff, Set.singleton_op]

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

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

Разделы

Аффилиация

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