English
If G is a detector, then for every X, Y and f: X → Y, whenever every G-to-Y morphism lifts along f (i.e., for all h: G → Y there exists a unique h': G → X with h' ∘ f = h), the morphism f is an isomorphism.
Русский
Если G является детектором, то для любых X, Y и f: X → Y, когда каждый морфизм G → Y поднимается через f (для каждого h: G → Y существует единственный h': G → X такой, что h' ∘ f = h), то f является изomорфизмом.
LaTeX
$$$\\mathrm{IsDetector}(G) \\Rightarrow \\forall X,Y\\; (f: X \\to Y),\\; (\\forall h: G \\to Y, \\exists! h': G \\to X,\\; h' \\circ f = h) \\to \\mathrm{IsIso}(f)$$$
Lean4
theorem «def» {G : C} : IsDetector G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : G ⟶ Y, ∃! h', h' ≫ f = h) → IsIso f :=
(isDetector_def _).1
