isCoseparating_op_iff — Mathlib

English

IsCoseparating 𝒢.op is equivalent to IsSeparating 𝒢.

Русский

IsCoseparating 𝒢.op эквивалентно IsSeparating 𝒢.

LaTeX

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

Lean4

theorem isCoseparating_op_iff (𝒢 : Set C) : IsCoseparating 𝒢.op ↔ IsSeparating 𝒢 :=
  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) _

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