ball_zero_absorbs_ball_zero — Mathlib

English

Reinterpreting a seminorm over a larger field 𝕜' as a seminorm over a subfield 𝕜 yields p.restrictScalars: p′(a,x) = p(a•x) with the embedding of scalars.

Русский

Переопределение семинормы над большим полем 𝕜' как семинормы над подполем 𝕜: p.restrictScalars(a,x) = p(a•x).

LaTeX

$$$\text{restrictScalars}(p) :\ for\ a\in 𝕜, x\in E,\; (p|_{𝕜'})(a x) = p(a\cdot x)$$$

Lean4

theorem ball_zero_absorbs_ball_zero (p : Seminorm 𝕜 E) {r₁ r₂ : ℝ} (hr₁ : 0 < r₁) :
    Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂) :=
  by
  rcases exists_pos_lt_mul hr₁ r₂ with ⟨r, hr₀, hr⟩
  refine .of_norm ⟨r, fun a ha x hx => ?_⟩
  rw [smul_ball_zero (norm_pos_iff.1 <| hr₀.trans_le ha), p.mem_ball_zero]
  rw [p.mem_ball_zero] at hx
  exact hx.trans (hr.trans_le <| by gcongr)

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