instDistribLattice — Mathlib

English

If β is a distributive lattice with bottom, then BotHom α β is a distributive lattice under the pointwise order.

Русский

Если β — распределительная решетка с нулём, то BotHom α β — распределительная решетка по точечному порядку.

LaTeX

$$$\\text{BotHom}(\\alpha,\\beta)\\text{ is a distributive lattice with bottom.}$$$

Lean4

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

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