dist_pi_const_le — Mathlib

English

If a,b ∈ α, then the distance between the constant functions a and b in the product is at most the distance between a and b in α.

Русский

Для констант a,b ∈ α расстояние между константами в произведении не больше расстояния между a и b в α.

LaTeX

$$$\mathrm{dist}(\lambda b,.a,\lambda b,.b) \le \mathrm{dist}(a,b).$$$

Lean4

theorem dist_pi_const_le (a b : α) : (dist (fun _ : β => a) fun _ => b) ≤ dist a b :=
  (dist_pi_le_iff dist_nonneg).2 fun _ => le_rfl

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