toInfHomClass — Mathlib

English

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

Русский

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

LaTeX

$$$$ [\text{SemilatticeInf }\alpha] [\text{SemilatticeInf }\beta] [\mathrm{OrderIsoClass } F \alpha \beta] \Rightarrow \mathrm{InfHomClass} F \alpha \beta. $$$$

Lean4

instance (priority := 100) toInfHomClass [SemilatticeInf α] [SemilatticeInf β] [OrderIsoClass F α β] :
    InfHomClass F α β :=
  { show OrderHomClass F α β from inferInstance with
    map_inf := fun f a b => eq_of_forall_le_iff fun c => by simp only [← map_inv_le_iff, le_inf_iff] }
    -- See note [lower instance priority]

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