edist_pi_const — Mathlib

English

If β is nonempty, the edistance between constant functions equals the distance between the constants: edist (fun _ : β => a) (fun _ : β => b) = edist a b.

Русский

Если β непусто, edist между константными функциями равен edist между константами: edist(постоянная_a, постоянная_b) = edist(a,b).

LaTeX

$$$$ edist (fun _ : \\beta => a) (fun _ : \\beta => b) = edist(a,b). $$$$

Lean4

@[simp]
theorem edist_pi_const [Nonempty β] (a b : α) : (edist (fun _ : β => a) fun _ => b) = edist a b :=
  Finset.sup_const univ_nonempty (edist a b)

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