isCoseparator_def — Mathlib

English

IsCoseparator G is equivalent to the condition that for all X,Y and f,g: X→Y, if for all h: Y→G, f ≫ h = g ≫ h, then f = g.

Русский

IsCoseparator G эквивалентно условию: для всех X,Y и f,g: X→Y, если для всех h: Y→G имеет f∘h = g∘h, то f = g.

LaTeX

$$$$\text{IsCoseparator}(G) \iff \forall X,Y:\, \forall f,g:X\to Y,\ (\forall h:Y\to G,\ f\circ h = g\circ h) \Rightarrow f = g.$$$$

Lean4

theorem isCoseparator_def (G : C) : IsCoseparator G ↔ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ h : Y ⟶ G, f ≫ h = g ≫ h) → f = g :=
  ⟨fun hG X Y f g hfg =>
    hG _ _ fun H hH h => by
      obtain rfl := Set.mem_singleton_iff.1 hH
      exact hfg h,
    fun hG _ _ _ _ hfg => hG _ _ fun _ => hfg _ (Set.mem_singleton _) _⟩

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