toBoundedLatticeHomClass — Mathlib

English

If α and β are co-Heyting algebras and F is a CoheytingHomClass F α β, then F inherits a bounded lattice hom-class structure; in particular, f(⊤) = ⊤ for all f ∈ F.

Русский

Если α и β — ко-Хейтинговые алгебры, и F — класс ко-Хейтинговых гомоморфизмов F α β, то F наследует структуру класса гомоморфизмов ограниченной решетки; в частности, f(⊤) = ⊤ для всех f ∈ F.

LaTeX

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

Lean4

instance (priority := 100) toBoundedLatticeHomClass [CoheytingAlgebra α] {_ : CoheytingAlgebra β}
    [CoheytingHomClass F α β] : BoundedLatticeHomClass F α β :=
  { ‹CoheytingHomClass F α β› with map_bot := fun f => by rw [← @sdiff_self α _ ⊤, ← sdiff_self, map_sdiff] }
    -- See note [lower instance priority]

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