English
Let W, W′, Q be morphism properties on a fixed category C. If W has the HasOfPrecompProperty with respect to Q, and W′ is contained in Q (W′ ≤ Q), then W has HasOfPrecompProperty with respect to W′. In words: the precomposition property is monotone in the right argument of the HasOfPrecompProperty construction.
Русский
Пусть на фиксированной категории C даны свойства морфизмов W, W′, Q. Если W удовлетворяет свойству HasOfPrecompProperty по отношению к Q, и W′ ⊆ Q, то W удовлетворяет HasOfPrecompProperty по отношению к W′. Иными словами: монотонность свойства предкомпозиции по правому аргументу.
LaTeX
$$$ (W \text{ HasOfPrecompProperty } Q) \wedge (W' \le Q) \\Rightarrow (W \text{ HasOfPrecompProperty } W'). $$$
Lean4
theorem of_le (Q : MorphismProperty C) [W.HasOfPrecompProperty Q] (hle : W' ≤ Q) : W.HasOfPrecompProperty W' where
of_precomp f g hg hfg := W.of_precomp (W' := Q) f g (hle _ hg) hfg
