edist_pi_const_le — Mathlib

English

The edistance between two constant functions is bounded above by the distance between their constant values: edist (const a) (const b) ≤ edist a b.

Русский

Эдистанс между двумя константными функциями не превосходит эдистанс между их константами: edist(const a, const b) ≤ edist(a,b).

LaTeX

$$$$ edist (\\text{const}_a) (\\text{const}_b) \\le edist(a,b). $$$$

Lean4

theorem edist_pi_const_le (a b : α) : (edist (fun _ : β => a) fun _ => b) ≤ edist a b :=
  edist_pi_le_iff.2 fun _ => le_rfl

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