prod_dist_eq_sup — Mathlib

English

For f, g ∈ WithLp ∞ (α × β), dist(f, g) equals the coordinatewise supremum distance: dist(f, g) = dist(f.fst, g.fst) ⊔ dist(f.snd, g.snd).

Русский

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

LaTeX

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

Lean4

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

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