instHeytingHomClass — Mathlib

English

The collection of Heyting algebra homomorphisms between α and β carries the structure of a HeytingHomClass, i.e., it preserves the operations sup, inf, bottom, and implication.

Русский

Набор гомоморфизмов алгебр Хейтинга α → β образует структуру HeytingHomClass, сохраняющую операции союз (∨), пересечение (∧), ноль и импликацию.

LaTeX

$$$\\text{HeytingHomClass}(\\mathrm{HeytingHom}(\\alpha,\\beta), \\alpha, \\beta)$$$

Lean4

instance instHeytingHomClass : HeytingHomClass (HeytingHom α β) α β
    where
  map_sup f := f.map_sup'
  map_inf f := f.map_inf'
  map_bot f := f.map_bot'
  map_himp := HeytingHom.map_himp'

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