instSemilatticeInf — Mathlib

English

The space α →ᵇ β carries both infimum and supremum operations making it a lattice-ordered structure under pointwise definitions.

Русский

Пространство ограниченных функций обладает и инфимуумом, и супремумом, образуя решеточно упорядченную структуру по точке.

LaTeX

$$$\\text{Inf/ Sup structure on } α \\to^b β$ with pointwise definitions$$

Lean4

instance instSemilatticeInf : SemilatticeInf (α →ᵇ β) :=
  fast_instance%DFunLike.coe_injective.semilatticeInf _ coe_inf

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