isCodetecting_unop_iff — Mathlib

English

Let 𝒢 be a set of objects in C. The collection 𝒢 unop in C^op codetects isomorphisms if and only if 𝒢 is detecting in C.

Русский

Пусть 𝒢 — множество объектов в C. Тогда 𝒢, просмотенное через unop в C^op, кодетектирует изоморфизмы тогда и только если 𝒢 детектирует в C.

LaTeX

$$$IsCodetecting(\mathcal{G}^{\mathrm{unop}}) \;\iff\; IsDetecting(\mathcal{G})$$$

Lean4

theorem isCodetecting_unop_iff {𝒢 : Set Cᵒᵖ} : IsCodetecting 𝒢.unop ↔ IsDetecting 𝒢 := by
  rw [← isDetecting_op_iff, Set.unop_op]

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