ball_pi' — Mathlib

English

A variant of dist_pi_le_iff for Real distances: 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) \le r \iff \forall b \in \mathrm{univ}, \mathrm{dist}(f(b),g(b)) \le r.$$$

Lean4

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

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