CategoryTheory.Limits.cokernel.condition_apply

theorem CategoryTheory.Limits.cokernel.condition_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.ConcreteCategory C] (x : (CategoryTheory.forget C).obj X), (CategoryTheory.Limits.cokernel.π f) (f x) = 0 x

The theorem `CategoryTheory.Limits.cokernel.condition_apply` states the following: For any categories `C`, `X`, `Y`, morphism `f` from `X` to `Y`, given that `C` has zero morphisms, `f` has a cokernel and `C` is a concrete category, then for any object `x` in the category `C` (when considered as an object of type via the forgetful functor), the composition of the map `f` followed by the cokernel map `π f` applied to `x` equals to the zero morphism applied to `x`. In other words, applying the cokernel map to the image of `x` under `f` gives us the zero object, reflecting the universal property of the cokernel in category theory.

More concisely: For any morphism `f` in a concrete category `C` with zero morphisms, if `f` has a cokernel, then for any object `x` in `C`, the composition of `f` and the cokernel map of `f` equals the zero morphism on `x`.