ofLE — Mathlib

English

If W1 ≤ W1' and W2 ≤ W2', then a factorization data for (W1, W2) induces a factorization data for (W1', W2').

Русский

Если W1 ≤ W1' и W2 ≤ W2', то факторизационные данные для (W1, W2) порождают факторизационные данные для (W1', W2').

LaTeX

$$$\text{ofLE} : W_1 \le W_1' \to W_2 \le W_2' \to W_1' .FactorizationData W_2'$$$

Lean4

/-- If `W₁ ≤ W₁'` and `W₂ ≤ W₂'`, then a functorial factorization for `W₁` and `W₂` induces
a functorial factorization for `W₁'` and `W₂'`. -/
def ofLE {W₁' W₂' : MorphismProperty C} (le₁ : W₁ ≤ W₁') (le₂ : W₂ ≤ W₂') : FunctorialFactorizationData W₁' W₂'
    where
  Z := data.Z
  i := data.i
  p := data.p
  hi f := le₁ _ (data.hi f)
  hp f := le₂ _ (data.hp f)

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