restrictScalars_closedBall — Mathlib

English

Restricting scalars to 𝕜 preserves closed balls of a seminorm around 0: the 0-centered closed ball of radius r for the restricted seminorm equals that for the original seminorm, for all r.

Русский

При ограничении скаляров до 𝕜 сохраняются замкнутые шары семинормы вокруг нуля: p.restrictScalars 𝕜 имеет такой же замкнутый шар, как и p.

LaTeX

$$$ (p\\restrictScalars 𝕜).closedBall = p.closedBall. $$$

Lean4

@[simp]
theorem restrictScalars_closedBall (p : Seminorm 𝕜' E) : (p.restrictScalars 𝕜).closedBall = p.closedBall :=
  rfl

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