toHeytingHomClass — Mathlib

English

An order isomorphism class provides a HeytingHomClass structure.

Русский

Изоморфизм порядка порождает структуру HeytingHomClass.

LaTeX

$$$ \text{OrderIsoClass } F α β \Rightarrow \text{HeytingHomClass } F α β$$$

Lean4

instance (priority := 100) toHeytingHomClass [HeytingAlgebra α] {_ : HeytingAlgebra β} [OrderIsoClass F α β] :
    HeytingHomClass F α β :=
  { OrderIsoClass.toBoundedLatticeHomClass with
    map_himp := fun f a b =>
      eq_of_forall_le_iff fun c => by
        simp only [← map_inv_le_iff, le_himp_iff]
        rw [← OrderIsoClass.map_le_map_iff f]
        simp }
    -- See note [lower instance priority]

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