of_le — Mathlib

English

If W.HasOfPostcompProperty Q holds and W' ≤ Q, then W.HasOfPostcompProperty W'.

Русский

Если W имеет свойство посткомпоновки относительно Q и W' ≤ Q, тогда W.HasOfPostcompProperty W'.

LaTeX

$$$[W.HasOfPostcompProperty Q] \land (W' \le Q) \Rightarrow W.HasOfPostcompProperty W'$$$

Lean4

theorem of_le (Q : MorphismProperty C) [W.HasOfPostcompProperty Q] (hle : W' ≤ Q) : W.HasOfPostcompProperty W' where
  of_postcomp f g hg hfg := W.of_postcomp (W' := Q) f g (hle _ hg) hfg

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