English
Same as above, specialized to a simplified form with base 1 or similar normalization.
Русский
То же самое, упрощено к базовой форме с единицей или аналогичной нормализацией.
LaTeX
$$$\text{Pairwise }\big(\mathrm{Disjoint} \text{ on } (n \mapsto \mathrm{Ioc}(a b^n, a b^{n+1}))\big)$$$
Lean4
@[to_additive]
theorem pairwise_disjoint_Ico_mul_zpow : Pairwise (Disjoint on fun n : ℤ => Ico (a * b ^ n) (a * b ^ (n + 1))) :=
by
simp +unfoldPartialApp only [Function.onFun]
simp_rw [Set.disjoint_iff]
intro m n hmn x hx
apply hmn
have hb : 1 < b := by
have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_lt hx.1.2
rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
have i1 := hx.1.1.trans_lt hx.2.2
have i2 := hx.2.1.trans_lt hx.1.2
rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff_right hb, Int.lt_add_one_iff] at i1 i2
exact le_antisymm i1 i2
