edist_mulIndicator — Mathlib

English

Reassertion: the distance between indicator-valued functions at x matches the NN-norm of the symmetric-difference indicator: edist(s.mulIndicator f x, t.mulIndicator f x) = ‖(s Δ t).mulIndicator f x‖₊.

Русский

Повторное утверждение: расстояние между индикаторами равно NN-норме индикатора симметрической разности.

LaTeX

$$$$ \\operatorname{edist}( s.mulIndicator f x, t.mulIndicator f x) = \\| (s \\Delta t).mulIndicator f x \\|_{+} $$$$

Lean4

@[to_additive]
theorem edist_mulIndicator (s t : Set α) (f : α → E) (x : α) :
    edist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖₊ := by
  rw [edist_nndist, nndist_mulIndicator]

Похожие утверждения