toCoheytingHomClass — Mathlib

English

An order isomorphism between Heyting algebras yields a CoheytingHomClass structure.

Русский

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

LaTeX

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

Lean4

instance (priority := 100) toCoheytingHomClass [BiheytingAlgebra α] {_ : BiheytingAlgebra β} [BiheytingHomClass F α β] :
    CoheytingHomClass F α β :=
  { ‹BiheytingHomClass F α β› with map_top := fun f => by rw [← @himp_self α _ ⊥, ← himp_self, map_himp] }

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