pairwise_disjoint_Ico_add_intCast

English

For any a ∈ α, the family n ∈ Z of intervals Ico(a + n, a + n + 1) are pairwise disjoint.

Русский

Для любого a ∈ α семейство целочисленных n: Ico(a + n, a + n + 1) попарно непересекается.

LaTeX

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

Lean4

theorem pairwise_disjoint_Ico_add_intCast : Pairwise (Disjoint on fun n : ℤ => Ico (a + n) (a + n + 1)) := by
  simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using pairwise_disjoint_Ico_add_zsmul a (1 : α)

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