toBiheytingHomClass — Mathlib

English

An order isomorphism class yields a BiheytingHomClass structure.

Русский

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

LaTeX

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

Lean4

instance (priority := 100) toBiheytingHomClass [BiheytingAlgebra α] {_ : BiheytingAlgebra β} [OrderIsoClass F α β] :
    BiheytingHomClass F α β :=
  {
    OrderIsoClass.toLatticeHomClass 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
    map_sdiff := fun f a b =>
      eq_of_forall_ge_iff fun c => by
        simp only [← le_map_inv_iff, sdiff_le_iff]
        rw [← OrderIsoClass.map_le_map_iff f]
        simp }

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