tosInfHomClass — Mathlib

English

There is an instance turning order isomorphisms into an inf-hom class.

Русский

Существует экземпляр, превращающий изоморфии порядка в класс гомоморфизмов, сохраняющих инфимы.

LaTeX

$$$ \\text{OrderIsoClass } F \\Rightarrow \\text{InfHomClass } F$$$

Lean4

instance (priority := 100) tosInfHomClass [CompleteLattice α] [CompleteLattice β] [OrderIsoClass F α β] :
    sInfHomClass F α β :=
  { show OrderHomClass F α β from inferInstance with
    map_sInf := fun f s =>
      eq_of_forall_le_iff fun c => by simp only [← map_inv_le_iff, le_sInf_iff, Set.forall_mem_image] }
    -- See note [lower instance priority]

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