instStrongHomClassOfIsAlgebraic — Mathlib

English

If L.IsAlgebraic, then there is a StrongHomClass structure for L, F, M, N given by the standard construction using HomClass.

Русский

Если L.IsAlgebraic, существует структура StrongHomClass для L, F, M, N, полученная стандартной конструкцией из HomClass.

LaTeX

$$$[L.IsAlgebraic] \\Rightarrow \\mathrm{StrongHomClass}\\ L\\ F\\ M\\ N$$$

Lean4

instance [L.IsAlgebraic] : StrongHomClass L (M →[L] N) M N :=
  HomClass.strongHomClassOfIsAlgebraic

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