sub_mem_ball — Mathlib

English

For a seminorm p on E and x1, x2, y ∈ E with radius r, x1 − x2 ∈ p.closedBall y r if and only if x1 ∈ p.closedBall (x2 + y) r.

Русский

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

LaTeX

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

Lean4

theorem sub_mem_ball (p : Seminorm 𝕜 E) (x₁ x₂ y : E) (r : ℝ) : x₁ - x₂ ∈ p.ball y r ↔ x₁ ∈ p.ball (x₂ + y) r := by
  simp_rw [mem_ball, sub_sub]

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