UniformOnFun — Mathlib

English

The type of functions from α to β equipped with the uniform structure of uniform convergence on a family 𝔖 of subsets of α is the underlying set α → β.

Русский

Тип функций α→β, оснащённый структурой равномерной сходимости по членам семейства 𝔖 подмножеств α, представляет собой множества функций α→β.

LaTeX

$$$\\mathrm{UniformOnFun}(\\alpha,\\beta,\\mathcal{S}) := \\alpha \\to \\beta$$$

Lean4

/-- The type of functions from `α` to `β` equipped with the uniform structure and topology of
uniform convergence on some family `𝔖` of subsets of `α`. We denote it `α →ᵤ[𝔖] β`. -/
@[nolint unusedArguments]
def UniformOnFun (α β : Type*) (_ : Set (Set α)) :=
  α → β

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