toSupHomClass — Mathlib

English

Given an order isomorphism, one obtains a SupHomClass between the underlying types.

Русский

Дана упорядоченная изоморфия; получается SupHomClass между базовыми типами.

LaTeX

$$$$ [\text{SemilatticeSup }\alpha] [\text{SemilatticeSup }\beta] [\mathrm{OrderIsoClass } F \alpha \beta] \Rightarrow \mathrm{SupHomClass} F \alpha \beta. $$$$

Lean4

instance (priority := 100) toSupHomClass [SemilatticeSup α] [SemilatticeSup β] [OrderIsoClass F α β] :
    SupHomClass F α β :=
  { show OrderHomClass F α β from inferInstance with
    map_sup := fun f a b => eq_of_forall_ge_iff fun c => by simp only [← le_map_inv_iff, sup_le_iff] }
    -- See note [lower instance priority]

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