toBiheytingHomClass — Mathlib

English

A bounded-lattice homomorphism class induces a BiheytingHomClass structure.

Русский

Класс гомоморфизмов ограниченной решетки индуцирует BiheytingHomClass.

LaTeX

$$$ \text{BoundedLatticeHomClass } F α β \Rightarrow \text{BiheytingHomClass } F α β$$$

Lean4

instance toBiheytingHomClass [BooleanAlgebra α] [BooleanAlgebra β] [BoundedLatticeHomClass F α β] :
    BiheytingHomClass F α β :=
  {
    ‹BoundedLatticeHomClass F α
        β› with
    map_himp := fun f a b => by rw [himp_eq, himp_eq, map_sup, (isCompl_compl.map _).compl_eq]
    map_sdiff := fun f a b => by rw [sdiff_eq, sdiff_eq, map_inf, (isCompl_compl.map _).compl_eq] }

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