Pointed.Hom.ext
theorem Pointed.Hom.ext : ∀ {X Y : Pointed} (x y : X.Hom Y), x.toFun = y.toFun → x = y
This theorem, `Pointed.Hom.ext`, states that for any two pointed spaces `X` and `Y`, and any two morphisms `x` and `y` from `X` to `Y` in the category of pointed spaces, if the underlying functions of `x` and `y` are equal, then `x` and `y` themselves are equal. In other words, in the category of pointed spaces, morphisms are determined entirely by their underlying functions.
More concisely: In the category of pointed spaces, two morphisms between pointed spaces with equal underlying functions are equal.
|
Pointed.Hom.map_point
theorem Pointed.Hom.map_point : ∀ {X Y : Pointed} (self : X.Hom Y), self.toFun X.point = Y.point
This theorem, named `Pointed.Hom.map_point`, states that for every homomorphism `self` from a pointed set `X` to another pointed set `Y`, the mapping function (`toFun`) of `self` applied to the distinguished point of `X` (`X.point`) equals the distinguished point of `Y` (`Y.point`). In other words, the homomorphism between two pointed sets preserves the distinguished points.
More concisely: For every homomorphism between pointed sets, the image of the distinguished point of the domain is the distinguished point of the codomain.
|