filter — Mathlib

English

The filter associated to a given 𝓕 via the UniformFun.basis construction.

Русский

Фильтр, полученный из 𝓕 через конструкцию UniformFun.basis.

LaTeX

$$$\\mathrm{UniformFun}.filter\\; α\\; β\\; 𝓕 := (\\mathrm{UniformFun}.basis α β 𝓕).\\mathrm{filter}$$$

Lean4

/-- For `𝓕 : Filter (β × β)`, this is the filter generated by the filter basis
`UniformFun.basis α β 𝓕`. For `𝓕 = 𝓤 β`, this will be the uniformity of uniform
convergence on `α`. -/
protected def filter (𝓕 : Filter <| β × β) : Filter ((α →ᵤ β) × (α →ᵤ β)) :=
  (UniformFun.basis α β 𝓕).filter

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