preimage_ball — Mathlib

English

Let i: ℕ → ℝ be the inclusion. The preimage of a real ball under i equals the corresponding ball in ℕ: i^{-1}(B_ℝ(x,r)) = B_ℕ(x,r).

Русский

Пусть i: ℕ → ℝ — включение. Преобразование i^{-1}(B_ℝ(x,r)) соответствует шару в ℕ: B_ℕ(x,r).

LaTeX

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

Lean4

theorem preimage_ball (x : ℕ) (r : ℝ) : (↑) ⁻¹' ball (x : ℝ) r = ball x r :=
  rfl

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