toBoundedLatticeHomClass — Mathlib

English

A Heyting homomorphism class F between Heyting algebras α and β induces a bounded lattice hom-class structure; in particular, top is preserved: f(⊤) = ⊤.

Русский

Класс гомоморфизмов Heyting между Heyting-алгебрами α и β индуцирует структуру класса гомоморфизмов ограниченной решетки; в частности, сохраняется верхний элемент: f(⊤) = ⊤.

LaTeX

$$$ \forall f,\ f(\top) = \top $$$

Lean4

instance (priority := 100) toBoundedLatticeHomClass [HeytingAlgebra α] {_ : HeytingAlgebra β} [HeytingHomClass F α β] :
    BoundedLatticeHomClass F α β :=
  { ‹HeytingHomClass F α β› with map_top := fun f => by rw [← @himp_self α _ ⊥, ← himp_self, map_himp] }
    -- See note [lower instance priority]

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