pairwise_disjoint_Ioo_intCast — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem pairwise_disjoint_Ioo_intCast : Pairwise (Disjoint on fun n : ℤ => Ioo (n : α) (n + 1)) := by
  simpa only [zero_add] using pairwise_disjoint_Ioo_add_intCast (0 : α)

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