prod_edist_eq_sup — Mathlib

English

For f, g ∈ WithLp ∞ (α × β), the distance is the maximum of the coordinate distances: edist(f, g) = edist(f.fst, g.fst) ⊔ edist(f.snd, g.snd).

Русский

Для f, g ∈ WithLp ∞ (α × β) расстояние равно максимуму расстояний по координатам: edist(f, g) = edist(f.fst, g.fst) ⊔ edist(f.snd, g.snd).

LaTeX

$$$$\operatorname{edist} f g = \operatorname{edist} f.fst g.fst \sqcup \operatorname{edist} f.snd g.snd$$$$

Lean4

theorem prod_edist_eq_sup (f g : WithLp ∞ (α × β)) : edist f g = edist f.fst g.fst ⊔ edist f.snd g.snd :=
  rfl

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