strongHomClassOfIsAlgebraic — Mathlib

English

If L is algebraic, then for any M,N and any F with FunLike F M N, the StrongHomClass structure is determined by HomClass (i.e., the construction of a strong homomorphism class from a homomorphism class).

Русский

Если L алгебраический, то для любых M,N и любого F с FunLike F M N существует структура StrongHomClass, которая выводится из HomClass (первичная конструкция сильного гомоморфизма).

LaTeX

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

Lean4

/-- Not an instance to avoid a loop. -/
theorem strongHomClassOfIsAlgebraic [L.IsAlgebraic] {F M N} [L.Structure M] [L.Structure N] [FunLike F M N]
    [HomClass L F M N] : StrongHomClass L F M N
    where
  map_fun := HomClass.map_fun
  map_rel _ _ := isEmptyElim

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