ball_pi — Mathlib

English

A ball in product space can be characterized using aPi-lt1: dist f g < r iff ∀ b, dist(f(b),g(b)) < r.

Русский

Окружность в произведении задаётся через компонентные неравенства: dist f g < r ⇔ ∀ b, dist(f(b),g(b)) < r.

LaTeX

$$$\mathrm{dist}(f,g) < r \iff \forall b, \mathrm{dist}(f(b),g(b)) < r.$$$

Lean4

/-- An open ball in a product space is a product of open balls. See also `ball_pi'`
for a version assuming `Nonempty β` instead of `0 < r`. -/
theorem ball_pi (x : ∀ b, X b) {r : ℝ} (hr : 0 < r) : ball x r = Set.pi univ fun b => ball (x b) r :=
  by
  ext p
  simp [dist_pi_lt_iff hr]

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