geomSum_injective — Mathlib

English

For n ≥ 2, the map s ↦ ∑_{i∈s} n^i is injective on Finset Nat.

Русский

Для n≥2 отображение s ↦ ∑_{i∈s} n^i инъективно на множествах Finset Nat.

LaTeX

$$Injective( s ↦ ∑_{i∈s} n^i ) for n ≥ 2$$

Lean4

theorem geomSum_injective {n : ℕ} (hn : 2 ≤ n) : Function.Injective (fun s : Finset ℕ ↦ ∑ i ∈ s, n ^ i) :=
  by
  intro _ _ h
  rwa [le_antisymm_iff, geomSum_le_geomSum_iff_toColex_le_toColex hn, geomSum_le_geomSum_iff_toColex_le_toColex hn, ←
    le_antisymm_iff] at h

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