isSeparating_op_iff — Mathlib

English

An equivalent statement asserting the same isomorphisms under op.

Русский

Эквивалентное высказывание, утверждающее то же самое изоморфизм под операцией.

LaTeX

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

Lean4

theorem isSeparating_op_iff (𝒢 : Set C) : IsSeparating 𝒢.op ↔ IsCoseparating 𝒢 :=
  by
  refine ⟨fun h𝒢 X Y f g hfg => ?_, fun h𝒢 X Y f g hfg => ?_⟩
  · refine Quiver.Hom.op_inj (h𝒢 _ _ fun G hG h => Quiver.Hom.unop_inj ?_)
    simpa only [unop_comp, Quiver.Hom.unop_op] using hfg _ (Set.mem_op.1 hG) _
  · refine Quiver.Hom.unop_inj (h𝒢 _ _ fun G hG h => Quiver.Hom.op_inj ?_)
    simpa only [op_comp, Quiver.Hom.op_unop] using hfg _ (Set.op_mem_op.2 hG) _

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