instHasFactorizationOfHasFunctorialFactorization

English

If HasFunctorialFactorization W₁ W₂ holds, then HasFactorization W₁ W₂ holds.

Русский

Если существует факторизационная структура для W₁ и W₂, то существует факторизация W₁ W₂.

LaTeX

$$[HasFunctorialFactorization W₁ W₂] ⇒ HasFactorization W₁ W₂$$

Lean4

instance [HasFunctorialFactorization W₁ W₂] : HasFactorization W₁ W₂ where
  nonempty_mapFactorizationData f := ⟨(functorialFactorizationData W₁ W₂).factorizationData f⟩

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