English
Preimages of cobounded sets under the algebra map are cobounded.
Русский
Образы предобразов кобондированных множеств через отображение алгебры являются кобондированными.
LaTeX
$$$\\operatorname{map}(\\mathrm{algebraMap}_{\\mathbb{K} \\to \\mathbb{K}'})(\\operatorname{cobounded}(\\mathbb{K})) \\le \\operatorname{cobounded}(\\mathbb{K}')$$$
Lean4
/-- Preimages of cobounded sets under the algebra map are cobounded.
-/
theorem algebraMap_cobounded_le_cobounded [NormOneClass 𝕜'] :
Filter.map (algebraMap 𝕜 𝕜') (Bornology.cobounded 𝕜) ≤ Bornology.cobounded 𝕜' :=
by
intro c hc
rw [Filter.mem_map, ← Bornology.isCobounded_def, ← Bornology.isBounded_compl_iff, isBounded_iff_forall_norm_le]
obtain ⟨s, hs⟩ := isBounded_iff_forall_norm_le.1 (Bornology.isBounded_compl_iff.2 (Bornology.isCobounded_def.1 hc))
use s
exact fun x hx ↦ by simpa [norm_algebraMap, norm_one] using hs ((algebraMap 𝕜 𝕜') x) hx
