sub_mem_closedBall — Mathlib

English

Same translation property for closed balls: x1 − x2 ∈ p.closedBall y r iff x1 ∈ p.closedBall (x2 + y) 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_closedBall (p : Seminorm 𝕜 E) (x₁ x₂ y : E) (r : ℝ) :
    x₁ - x₂ ∈ p.closedBall y r ↔ x₁ ∈ p.closedBall (x₂ + y) r := by simp_rw [mem_closedBall, sub_sub]

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