isSeparating_unop_iff

Mathlib.CategoryTheory.Generator.Basic

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

English

The separating property is equivalent to its unop version.

Русский

Свойство разделяющего равно его версии через unop.

LaTeX

$$$IsSeparating(𝒢.unop) \iff IsCoseparating(𝒢)$$$

Lean4

theorem isSeparating_unop_iff (𝒢 : Set Cᵒᵖ) : IsSeparating 𝒢.unop ↔ IsCoseparating 𝒢 := by
  rw [← isCoseparating_op_iff, Set.unop_op]

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

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

Разделы

Аффилиация

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