geomSum_le_geomSum_iff_toColex_le_toColex

English

For n ≥ 2, s ↦ ∑_{k ∈ ofColex s} n^k is strictly monotone with respect to the Colex order.

Русский

Для n≥2 отображение s ↦ ∑_{k ∈ ofColex s} n^k строго возрастает по колексORD.

LaTeX

$$$\text{StrictMono}(f) \Rightarrow \text{StrictMono}(s \mapsto \sum_{k \in ofColex(s)} n^k)$ with $n\ge 2$$$

Lean4

/-- For finsets of naturals, the colexicographic order is equivalent to the order induced by the
`n`-ary expansion. -/
theorem geomSum_le_geomSum_iff_toColex_le_toColex (hn : 2 ≤ n) :
    ∑ k ∈ s, n ^ k ≤ ∑ k ∈ t, n ^ k ↔ toColex s ≤ toColex t :=
  (geomSum_ofColex_strictMono hn).le_iff_le

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