English
Let s,t ⊆ α and f: α → E. Then for every x ∈ α, the distance between the indicator values at x equals the norm of the indicator of the symmetric difference at x: dist(s.mulIndicator f x, t.mulIndicator f x) = ‖(s Δ t).mulIndicator f x‖.
Русский
Пусть s,t ⊆ α и f: α → E. Тогда для каждого x в α расстояние между значениями индикаторов в x равно норме индикатора симметрической разности: dist(s.mulIndicator f x, t.mulIndicator f x) = ‖(s Δ t).mulIndicator f x‖.
LaTeX
$$$\operatorname{dist}(s\cdot\mathrm{Indicator}\, f\, x, t\cdot\mathrm{Indicator}\, f\, x) = \| (s \Delta t)\cdot\mathrm{Indicator}\, f\, x \|$$$
Lean4
@[to_additive]
theorem dist_mulIndicator (s t : Set α) (f : α → E) (x : α) :
dist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖ := by
rw [dist_eq_norm_div, Set.apply_mulIndicator_symmDiff norm_inv']
