tosSupHomClass — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance (priority := 100) tosSupHomClass [CompleteLattice α] [CompleteLattice β] [OrderIsoClass F α β] :
    sSupHomClass F α β :=
  { show OrderHomClass F α β from inferInstance with
    map_sSup := fun f s =>
      eq_of_forall_ge_iff fun c => by simp only [← le_map_inv_iff, sSup_le_iff, Set.forall_mem_image] }
    -- See note [lower instance priority]

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