English
Restricting scalars preserves vonNBoundedness in the nontrivial scalar case.
Русский
Сохранение ограниченности фон Неймана при сокращении поля скаляров в несоответствующем случае.
LaTeX
$$$\\operatorname{IsVonNBounded}_{\\mathbb{k}'}(s) \\Rightarrow \\operatorname{IsVonNBounded}_{\\mathbb{k}}(s)$$$
Lean4
theorem isVonNBounded {s : Set E} (hs : TotallyBounded s) : Bornology.IsVonNBounded 𝕜 s := by
if h : ∃ x : 𝕜, 1 < ‖x‖ then
letI : NontriviallyNormedField 𝕜 := ⟨h⟩
rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero] at hs
intro U hU
have h : Filter.Tendsto (fun x : E × E => x.fst + x.snd) (𝓝 0) (𝓝 0) := continuous_add.tendsto' _ _ (zero_add _)
have h' := (nhds_basis_balanced 𝕜 E).prod (nhds_basis_balanced 𝕜 E)
simp_rw [← nhds_prod_eq, id] at h'
rcases h.basis_left h' U hU with ⟨x, hx, h''⟩
rcases hs x.snd hx.2.1 with ⟨t, ht, hs⟩
refine Absorbs.mono_right ?_ hs
rw [ht.absorbs_biUnion]
have hx_fstsnd : x.fst + x.snd ⊆ U := add_subset_iff.mpr fun z1 hz1 z2 hz2 ↦ h'' <| mk_mem_prod hz1 hz2
refine fun y _ => Absorbs.mono_left ?_ hx_fstsnd
exact Absorbent.vadd_absorbs (absorbent_nhds_zero hx.1.1) hx.2.2.absorbs_self
else
haveI : BoundedSpace 𝕜 := ⟨Metric.isBounded_iff.2 ⟨1, by simp_all [dist_eq_norm]⟩⟩
exact Bornology.IsVonNBounded.of_boundedSpace
