English
Restricting scalars to 𝕜 preserves open balls of a seminorm around 0: the 0-centered open ball of radius r for the restricted seminorm equals that for the original seminorm, for all r > 0.
Русский
При ограничении скаляров до 𝕜 сохраняются открытые шарa семинормы вокруг нуля: p.restrictScalars 𝕜 имеет тот же открытый шар вокруг 0 радиуса r, что и p, при всех r > 0.
LaTeX
$$$ (p\\restrictScalars 𝕜).\\mathrm{ball} = p.\\mathrm{ball}. $$$
Lean4
@[simp]
theorem restrictScalars_ball (p : Seminorm 𝕜' E) : (p.restrictScalars 𝕜).ball = p.ball :=
rfl