English
Let f, g be in WithLp 0 (α × β). Then the distance edist(f, g) counts, coordinatewise, how many components differ: it equals 0 in a coordinate if that coordinate agrees, and 1 otherwise; overall, edist(f, g) is the sum of these two coordinate indicators.
Русский
Пусть f, g ∈ WithLp 0 (α × β). Тогда расстояние edist(f, g) по существу считается координатно: в каждой координате 0, если координаты совпадают, и 1 иначе; суммарно edist(f, g) равняется сумме двух таких индикаторов.
LaTeX
$$$$\operatorname{edist} f g = \big(\text{if } \operatorname{edist}(f.fst, g.fst) = 0 \ \text{then } 0 \ \text{else } 1\big) + \big(\text{if } \operatorname{edist}(f.snd, g.snd) = 0 \ \text{then } 0 \ \text{else } 1\big)$$$$
Lean4
@[simp]
theorem prod_edist_eq_card (f g : WithLp 0 (α × β)) :
edist f g = (if edist f.fst g.fst = 0 then 0 else 1) + (if edist f.snd g.snd = 0 then 0 else 1) := by
convert if_pos rfl
