toHeytingHomClass — Mathlib

English

An order isomorphism between Heyting algebras induces a Heyting homomorphism class.

Русский

Изоморфизм порядка между Хейтинговыми алгебрами индуцирует класс гомоморфизмов Хейтинга.

LaTeX

$$$ \text{If } F \text{ is an order isomorphism class between } α,β, \text{ then } F \text{ induces a HeytingHomClass.}$$$

Lean4

instance (priority := 100) toHeytingHomClass [BiheytingAlgebra α] {_ : BiheytingAlgebra β} [BiheytingHomClass F α β] :
    HeytingHomClass F α β :=
  { ‹BiheytingHomClass F α β› with
    map_bot := fun f => by rw [← @sdiff_self α _ ⊤, ← sdiff_self, BiheytingHomClass.map_sdiff] }
    -- See note [lower instance priority]

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