schnirelmannDensity_congr' — Mathlib

English

If A and B have the same membership for all n > 0, then their Schnirelmann densities are equal.

Русский

Если множества A и B совпадают по принадлежности для всех n > 0, то их плотности Шниррельмана равны.

LaTeX

$$\\forall n>0,\\ (n \\in A \\iff n \\in B) \\Rightarrow \\operatorname{schnirelmannDensity}(A) = \\operatorname{schnirelmannDensity}(B)$$

Lean4

theorem schnirelmannDensity_congr' {B : Set ℕ} [DecidablePred (· ∈ B)] (h : ∀ n > 0, n ∈ A ↔ n ∈ B) :
    schnirelmannDensity A = schnirelmannDensity B := by rw [schnirelmannDensity, schnirelmannDensity]; congr;
  ext ⟨n, hn⟩; congr 3; ext x; simp_all

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