preimage_metric_ball — Mathlib

English

For any seminorm p, the preimage of the metric ball of radius r around 0 equals the set { x | p(x) < r }. In symbols: p^{-1}(Metric.ball 0 r) = { x | p x < r }.

Русский

Для любой полупр. нормы p предобраз метрического шара радиуса r вокруг 0 равен множеству {x | p(x) < r}. То есть p^{-1}(Metric.ball 0 r) = { x | p x < r }.

LaTeX

$$$p^{-1}(\mathrm{Metric.ball} 0 r) = \{ x \mid p x < r \}$$$

Lean4

theorem preimage_metric_ball {r : ℝ} : p ⁻¹' Metric.ball 0 r = {x | p x < r} :=
  by
  ext x
  simp only [mem_setOf, mem_preimage, mem_ball_zero_iff, Real.norm_of_nonneg (apply_nonneg p _)]

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