nndist_pi_const_le — Mathlib

English

For constant functions with values a,b, the nonnegative distance between them equals the base nndist between a and b.

Русский

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

LaTeX

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

Lean4

theorem nndist_pi_const_le (a b : α) : (nndist (fun _ : β => a) fun _ => b) ≤ nndist a b :=
  nndist_pi_le_iff.2 fun _ => le_rfl

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