instLatticeHomClass — Mathlib

English

Every lattice homomorphism preserves both joins and meets; hence they form a class of morphisms preserving both operations.

Русский

Каждый гомоморфизм решетки сохраняет как объединения, так и пересечения; следовательно, множество таких гомоморфизмов образует класс сохраняющих обе операции.

LaTeX

$$$\forall f:\mathrm{LatticeHom}(\alpha,\beta),\ \forall a,b\in \alpha,\ f(a\lor b)=f(a)\lor f(b) \ \text{and}\ \ f(a\land b)=f(a)\land f(b).$$$

Lean4

instance : LatticeHomClass (LatticeHom α β) α β
    where
  map_sup f := f.map_sup'
  map_inf f := f.map_inf'

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