ofFun_prod — Mathlib

English

Let 𝔖 be a nonempty directed family. Then the neighborhood basis at 1 in UniformOnFun α G 𝔖 is given by pairs SV = (S, V) with S ∈ 𝔖 and V ∈ nhds 1 in G, and the basic neighborhoods are {f : α →ᵤ[𝔖] G | ∀ x ∈ S, f(x) ∈ V}.

Русский

Пусть 𝔖 — направленное непустое семейство; базис окрестностей 1 в UniformOnFun α G 𝔖 задается парами (S,V) с S ∈ 𝔖 и V ∈ nhds 1 в G, а базисные окрестности — {f | ∀ x ∈ S, f(x) ∈ V}.

LaTeX

$$$\text{nhds}_1 (\mathrm{UniformOnFun} \; α \; G \; 𝔖) = \{SV : SV.1 ∈ 𝔖 \land SV.2 ∈ (\mathcal{nhds}(1) : Filter G)\}.$$$$

Lean4

@[to_additive (attr := simp)]
theorem ofFun_prod {β : Type*} [CommMonoid β] {f : ι → α → β} (I : Finset ι) :
    ofFun 𝔖 (∏ i ∈ I, f i) = ∏ i ∈ I, ofFun 𝔖 (f i) :=
  rfl

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