instStrongHomClass — Mathlib

English

Let L be a language, and M,N,P,Q be L-structures. Then the collection of L-equivalences from M to N carries the natural structure of a strong homomorphism class, with the action on function symbols and relation symbols given by the standard map_fun and map_rel operations.

Русский

Пусть L — язык, а M, N, P, Q — структуры над L. Тогда множество L-эквивалентностей между M и N образуется в естественную структуру класса сильных гомоморфизмов между M и N, определяемую действием на символы функций и отношений через соответствующие операции map_fun и map_rel.

LaTeX

$$$\operatorname{StrongHomClass}_L\bigl(M \cong_L N\bigr)\; M\; N$$$

Lean4

instance : StrongHomClass L (M ≃[L] N) M N where
  map_fun := map_fun'
  map_rel := map_rel'

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