pairwise_disjoint_Ico_intCast — Mathlib

English

Let α be a ring with a compatible order. Then the family of half-open intervals Ico(n, n+1) inside α, indexed by n ∈ Z, are pairwise disjoint; i.e., for any distinct integers n and m, the sets Ico(n, n+1) and Ico(m, m+1) do not overlap.

Русский

Пусть α — кольцо с упорядочением, совместимым с операциями. Тогда множество Ico(n, n+1) внутри α (для n ∈ ℤ) попарно непересекаются; то есть для любых различных n,m ∈ ℤ пересечение Ico(n, n+1) и Ico(m, m+1) пусто.

LaTeX

$$$\forall n,m \in \mathbb{Z},\ n \neq m \implies Ico(n:\alpha, n+1) \cap Ico(m:\alpha, m+1) = \varnothing$$$

Lean4

theorem pairwise_disjoint_Ico_intCast : Pairwise (Disjoint on fun n : ℤ => Ico (n : α) (n + 1)) := by
  simpa only [zero_add] using pairwise_disjoint_Ico_add_intCast (0 : α)

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