English
For sets s,t ⊆ α, function f: α → E, and x ∈ α, the distance between the indicator-valued functions at x equals the NN-norm of the indicator of the symmetric difference: nndist(s.mulIndicator f x, t.mulIndicator f x) = ‖(s Δ t).mulIndicator f x‖₊.
Русский
Для множеств s,t ⊆ α, отображения f: α → E и элемента x ∈ α расстояние между соответствующими значениями индикаторов в точке x равно NN-норме индикатора симметрической разности: nndist(...) = ‖(s Δ t).mulIndicator f x‖₊.
LaTeX
$$$$ \\operatorname{nndist}( s.mulIndicator f x, t.mulIndicator f x) = \\| (s \\Delta t).mulIndicator f x \\|_{+} $$$$
Lean4
@[to_additive]
theorem nndist_mulIndicator (s t : Set α) (f : α → E) (x : α) :
nndist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖₊ :=
NNReal.eq <| dist_mulIndicator s t f x
