schnirelmannDensity_diff_singleton_zero

English

Removing the element 0 from A does not change its Schnirelmann density.

Русский

Удаление элемента 0 из A не меняет плотности Шниррельмана.

LaTeX

$$\\operatorname{schnirelmannDensity}(A \\setminus \\{0\\}) = \\operatorname{schnirelmannDensity}(A)$$

Lean4

/-- The Schnirelmann density is unaffected by removing `0`. -/
theorem schnirelmannDensity_diff_singleton_zero [DecidablePred (· ∈ A \ {0})] :
    schnirelmannDensity (A \ {0}) = schnirelmannDensity A :=
  schnirelmannDensity_congr' (by aesop)

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