toOrderHomClass — Mathlib

English

If F preserves binary infima on lattices, then F is an OrderHomClass.

Русский

Если F сохраняет бинарные наибольшие элементы, то F является OrderHomClass.

LaTeX

$$$$ [Lattice \alpha] [Lattice \beta] [LatticeHomClass F \alpha \beta] \Rightarrow \mathrm{OrderHomClass} F \alpha \beta. $$$$

Lean4

instance (priority := 100) toOrderHomClass [SemilatticeInf α] [SemilatticeInf β] [InfHomClass F α β] :
    OrderHomClass F α β :=
  { ‹InfHomClass F α β› with map_rel := fun f a b h => by rw [← inf_eq_left, ← map_inf, inf_eq_left.2 h] }
    -- See note [lower instance priority]

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