restrictScalars_ball — Mathlib

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

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