closedBall_add_closedBall_subset — Mathlib

English

For a seminorm p on E and points x1, x2 ∈ E, radii y ∈ R, one has x1 − x2 ∈ p.ball y r if and only if x1 ∈ p.ball (x2 + y) r.

Русский

Пусть p — семинорм на E и x1, x2 ∈ E, y ∈ E, радиус r. Тогда x1 − x2 ∈ p.ball(y,r) эквивалентно x1 ∈ p.ball(x2 + y, r).

LaTeX

$$$(x_1 - x_2) \in p.ball(y,r) \iff x_1 \in p.ball(x_2 + y, r)$$$

Lean4

theorem closedBall_add_closedBall_subset (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) (x₁ x₂ : E) :
    p.closedBall (x₁ : E) r₁ + p.closedBall (x₂ : E) r₂ ⊆ p.closedBall (x₁ + x₂) (r₁ + r₂) :=
  by
  rintro x ⟨y₁, hy₁, y₂, hy₂, rfl⟩
  rw [mem_closedBall, add_sub_add_comm]
  exact (map_add_le_add p _ _).trans (add_le_add hy₁ hy₂)

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