isSeparator_def — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isSeparator_def (G : C) : IsSeparator G ↔ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ h : G ⟶ X, h ≫ f = h ≫ g) → 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 _) _⟩

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