Ico_inter_Ico_consecutive — Mathlib

English

For any a, b, c in the ordered set, the intersection Ico(a,b) ∩ Ico(b,c) is empty; these consecutive half-open intervals do not overlap.

Русский

Для любых a, b, c в упорядоченном множестве пересечение Ico(a,b) ∩ Ico(b,c) пусто; последовательные полубытики не пересекаются.

LaTeX

$$$$ Ico(a,b) \cap Ico(b,c) = \emptyset $$$$

Lean4

@[simp]
theorem Ico_inter_Ico_consecutive (a b c : α) : Ico a b ∩ Ico b c = ∅ :=
  (Ico_disjoint_Ico_consecutive a b c).eq_bot

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