toCoheytingHomClass — Mathlib

English

An order isomorphism class yields a CoheytingHomClass structure.

Русский

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

LaTeX

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

Lean4

instance (priority := 100) toCoheytingHomClass [CoheytingAlgebra α] {_ : CoheytingAlgebra β} [OrderIsoClass F α β] :
    CoheytingHomClass F α β :=
  { OrderIsoClass.toBoundedLatticeHomClass with
    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 }
    -- See note [lower instance priority]

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