isUniformEmbedding_restrictScalars

English

The restriction of scalars map forgets the extra field structure in a uniformly continuous way: restricting the base field is uniformly continuous.

Русский

Сведение по скалярам с сохранением униформной структуры является равномерно непрерывным переходом.

LaTeX

$$$UniformContinuous(\\mathrm{restrictScalars}\\, 𝕜')$$$

Lean4

theorem isUniformEmbedding_restrictScalars : IsUniformEmbedding (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F)) :=
  by
  rw [← isUniformEmbedding_toUniformOnFun.of_comp_iff]
  convert isUniformEmbedding_toUniformOnFun using 4 with s
  exact ⟨fun h ↦ h.extend_scalars _, fun h ↦ h.restrict_scalars _⟩

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