isCoseparating_unop_iff

Mathlib.CategoryTheory.Generator.Basic

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

English

Unop version: IsCoseparating 𝒢.unop is equivalent to IsSeparating 𝒢.

Русский

Версия через unop: IsCoseparating 𝒢.unop эквивалентно IsSeparating 𝒢.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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