English
For f, g ∈ WithLp 0 (α × β), the distance dist(f, g) equals the sum of two indicator terms (0 or 1) depending on whether the respective coordinates differ: dist(f, g) = (if dist f.fst g.fst = 0 then 0 else 1) + (if dist f.snd g.snd = 0 then 0 else 1).
Русский
Для f, g ∈ WithLp 0 (α × β) расстояние dist(f, g) равно сумме двух индикаторов несходности координат: dist(f, g) = (если dist f.fst g.fst = 0 то 0, иначе 1) + (если dist f.snd g.snd = 0 то 0, иначе 1).
LaTeX
$$$$\operatorname{dist} f g = \big(\text{if } \operatorname{dist} f.fst g.fst = 0 \ \text{then } 0 \ \text{else } 1\big) + \big(\text{if } \operatorname{dist} f.snd g.snd = 0 \ \text{then } 0 \ \text{else } 1\big)$$$$
Lean4
theorem prod_dist_eq_card (f g : WithLp 0 (α × β)) :
dist f g = (if dist f.fst g.fst = 0 then 0 else 1) + (if dist f.snd g.snd = 0 then 0 else 1) := by
convert if_pos rfl
