pairwise_disjoint_Ioo_mul_zpow — Mathlib

English

As above, for general a,b in a commutative group with ordered monoid: the family n ↦ Ioc(a b^n, a b^{n+1}) is pairwise disjoint.

Русский

Как выше, для общих a,b в коммутативной группе с упорядоченным моноидом: семейство n ↦ Ioc(a b^n, a b^{n+1}) попарно непересекается.

LaTeX

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

Lean4

@[to_additive]
theorem pairwise_disjoint_Ioo_mul_zpow : Pairwise (Disjoint on fun n : ℤ => Ioo (a * b ^ n) (a * b ^ (n + 1))) :=
  fun _ _ hmn => (pairwise_disjoint_Ioc_mul_zpow a b hmn).mono Ioo_subset_Ioc_self Ioo_subset_Ioc_self

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