schnirelmannDensity_insert_zero — Mathlib

English

The Schnirelmann density is unchanged by inserting 0 into A.

Русский

Плотность Шниррельмана не меняется при добавлении нуля в A.

LaTeX

$$\\operatorname{schnirelmannDensity}(\\operatorname{insert}(0,A)) = \\operatorname{schnirelmannDensity}(A)$$

Lean4

/-- The Schnirelmann density is unaffected by adding `0`. -/
@[simp]
theorem schnirelmannDensity_insert_zero [DecidablePred (· ∈ insert 0 A)] :
    schnirelmannDensity (insert 0 A) = schnirelmannDensity A :=
  schnirelmannDensity_congr' (by aesop)

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