English
If S is von Neumann bounded in the space of uniform convergence CLM σ F 𝔖, then for every s ∈ 𝔖, the set of all values f(x) with f ∈ S and x ∈ s is von Neumann bounded in F.
Русский
Пусть S von Neumann ограничено в пространстве UniformConvergenceCLM σ F 𝔖. Тогда для каждого s ∈ 𝔖 множество { f(x) : f ∈ S, x ∈ s } является von Neumann ограниченным в F.
LaTeX
$$$$ IsVonNBounded_R\big( Set.image2 (\lambda f x, f(x))\; S\; s \big). $$$$
Lean4
theorem isVonNBounded_image2_apply {R : Type*} [SeminormedRing R] [TopologicalSpace F] [IsTopologicalAddGroup F]
[DistribMulAction R F] [ContinuousConstSMul R F] [SMulCommClass 𝕜₂ R F] {𝔖 : Set (Set E)}
{S : Set (UniformConvergenceCLM σ F 𝔖)} (hS : IsVonNBounded R S) {s : Set E} (hs : s ∈ 𝔖) :
IsVonNBounded R (Set.image2 (fun f x ↦ f x) S s) :=
by
intro U hU
filter_upwards [hS (eventually_nhds_zero_mapsTo σ hs hU)] with c hc
rw [image2_subset_iff]
intro f hf x hx
rcases hc hf with ⟨g, hg, rfl⟩
exact smul_mem_smul_set (hg hx)
