preimage_metric_closedBall — Mathlib

English

Similarly, p^{-1}(Metric.closedBall 0 r) = { x | p x ≤ r }.

Русский

Аналогично, предобраз p через метрический закрытый шар: p^{-1}(Metric.closedBall 0 r) = { x | p x ≤ r }.

LaTeX

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

Lean4

theorem preimage_metric_closedBall {r : ℝ} : p ⁻¹' Metric.closedBall 0 r = {x | p x ≤ r} :=
  by
  ext x
  simp only [mem_setOf, mem_preimage, mem_closedBall_zero_iff, Real.norm_of_nonneg (apply_nonneg p _)]

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