instDistribLattice — Mathlib

English

If β is a distributive lattice with top, then TopHom α β is a distributive lattice with the pointwise definitions.

Русский

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

LaTeX

$$$\\text{If } \\beta\\ \\text{is a distributive lattice with top, then } \\text{TopHom}(\\alpha,\\beta) \\text{ is a distributive lattice.}$$$

Lean4

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

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