geomSum_lt_geomSum_iff_toColex_lt_toColex

English

For n ≥ 2, s,t finite, ∑_{i∈s} n^i < ∑_{i∈t} n^i iff toColex s < toColex t.

Русский

Для n≥2, для конечных s,t: меньше ли сумма по s, чем по t, эквивалентно меньшему колекс порядку: toColex s < toColex t.

LaTeX

$$$\sum_{i \in s} n^i < \sum_{i \in t} n^i \iff toColex s < toColex t$ (при $n\ge 2$)$$

Lean4

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

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