dist_le_pi_dist — Mathlib

English

An open ball in a product space is the product of open balls when r>0.

Русский

Открытая окружность в произведении равна произведению открытых окружностей по компонентам, если r>0.

LaTeX

$$$\mathrm{ball}(x,r) = \mathrm{Set.pi}\,\mathrm{univ}\, (\lambda b. \mathrm{ball}(x(b),r)).$$$

Lean4

theorem dist_le_pi_dist (f g : ∀ b, X b) (b : β) : dist (f b) (g b) ≤ dist f g := by
  simp only [dist_nndist, NNReal.coe_le_coe, nndist_le_pi_nndist f g b]

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