instLattice — Mathlib

English

If β is a lattice with a top, then TopHom α β forms a lattice under the pointwise order and pointwise inf/sup.

Русский

Если β — решетка с верхней границей, то TopHom α β образует решётку с точечным порядком и точечными inf/sup.

LaTeX

$$$\\text{TopHom}(\\alpha,\\beta)\\text{ is a lattice with } (f\\wedge g)(a)=f(a)\\wedge g(a), (f\\vee g)(a)=f(a)\\vee g(a).$$$

Lean4

instance [Lattice β] [OrderTop β] : Lattice (TopHom α β) :=
  DFunLike.coe_injective.lattice _ (fun _ _ => rfl) fun _ _ => rfl

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