pairwise_disjoint_Ico_zpow — Mathlib

English

Let b be a positive element; the family n ↦ Ico(b^n, b^{n+1}) (n ∈ Z) is pairwise disjoint.

Русский

Пусть b положителен; семейство n ↦ Ico(b^n, b^{n+1}) (n ∈ Z) попарно непересекается.

LaTeX

$$$\text{Pairwise }\big(\mathrm{Disjoint} \text{ on } (n \mapsto \mathrm{Ico}(b^n, b^{n+1}))\big)$$$

Lean4

@[to_additive]
theorem pairwise_disjoint_Ico_zpow : Pairwise (Disjoint on fun n : ℤ => Ico (b ^ n) (b ^ (n + 1))) := by
  simpa only [one_mul] using pairwise_disjoint_Ico_mul_zpow 1 b

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