English
Let α be a topological space and β a lattice with a solid norm and an ordered additive structure. Then the set of bounded continuous functions from α to β, denoted α →ᵇ β, forms a lattice under the pointwise order: for f, g ∈ α →ᵇ β, (f ⊔ g)(x) = f(x) ⊔ g(x) and (f ⊓ g)(x) = f(x) ⊓ g(x) for all x ∈ α, and f ≤ g iff ∀ x, f(x) ≤ g(x).
Русский
Пусть α — топологическое множество и β — решетка с твердой нормой и упорядоченной аддитивной структурой. Тогда множество ограниченно непрерывных функций α → β образует решётку по точечному порядку: для f, g ∈ α →ᵇ β определяем f ⊔ g по значению в каждой точке, и f ≤ g эквивалентно f(x) ≤ g(x) для всех x.
LaTeX
$$$\forall f,g \in \alpha \to^b \beta,\; f \le g \iff \forall x, f(x) \le g(x),\quad (f \lor g)(x)=f(x) \lor g(x),\; (f \land g)(x)=f(x) \land g(x).$$$
Lean4
instance instLattice : Lattice (α →ᵇ β) :=
fast_instance%DFunLike.coe_injective.lattice _ coe_sup coe_inf
