preimage_closedBall — Mathlib

English

Similarly, the preimage of a real closed ball under the inclusion equals the closed ball in ℕ: i^{-1}(closedBallℝ(x,r)) = closedBallℕ(x,r).

Русский

Аналогично, прообраз замкнутого шара в ℝ равен замкнутому шару в ℕ.

LaTeX

$$$i^{-1}(\mathrm{closedBall}_{\mathbb{R}}(x,r)) = \mathrm{closedBall}_{\mathbb{N}}(x,r)$$$

Lean4

theorem preimage_closedBall (x : ℕ) (r : ℝ) : (↑) ⁻¹' closedBall (x : ℝ) r = closedBall x r :=
  rfl

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