ball_sup — Mathlib

English

A variant of the previous relation suitable for simplification rules: (c • p).closedBall x r = p.closedBall x (r / c) when c > 0.

Русский

Вариант предыдущего соотношения, пригодный для правил упрощения: (c • p).closedBall x r = p.closedBall x (r / c) при c > 0.

LaTeX

$$$ (c \\cdot p).closedBall\\, x\\, r = p.closedBall\\, x\\, \\frac{r}{c} $$$

Lean4

theorem ball_sup (p : Seminorm 𝕜 E) (q : Seminorm 𝕜 E) (e : E) (r : ℝ) : ball (p ⊔ q) e r = ball p e r ∩ ball q e r :=
  by simp_rw [ball, ← Set.setOf_and, coe_sup, Pi.sup_apply, sup_lt_iff]

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