P_Product_Metric_is_Metric_v2
Provedp-product-metricsproofwiki
The p-product metric on a product of metric spaces satisfies the triangle inequality.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem P_Product_Metric_is_Metric_v2 {α : Type _} {β : Type _} [MetricSpace α] [MetricSpace β] (x y z : α × β) : dist x z ≤ dist x y + dist y z := by sorrySource