dist_pi_const — Mathlib

English

If β is nonempty, the NN-distance between constant functions a and b equals the NN-distance between a and b in α.

Русский

Пусть β непусто; расстояние между константами в произведении равно расстоянию между их значениями.

LaTeX

$$$\mathrm{nndist}(\lambda_! b, a, \lambda_! b, b) = \mathrm{nndist}(a,b).$$$

Lean4

@[simp]
theorem dist_pi_const [Nonempty β] (a b : α) : (dist (fun _ : β => a) fun _ => b) = dist a b := by
  simpa only [dist_edist] using congr_arg ENNReal.toReal (edist_pi_const a b)

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