schnirelmannDensity_congr — Mathlib

English

If A = B, then schnirelmannDensity(A) = schnirelmannDensity(B).

Русский

Если A равно B, то плотности Шниррельмана совпадают.

LaTeX

$$A = B \\Rightarrow \\operatorname{schnirelmannDensity}(A) = \\operatorname{schnirelmannDensity}(B)$$

Lean4

theorem schnirelmannDensity_congr {B : Set ℕ} [DecidablePred (· ∈ B)] (h : A = B) :
    schnirelmannDensity A = schnirelmannDensity B :=
  schnirelmannDensity_congr' (by simp_all)

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