finite_diff_iUnion_Ioo — Mathlib

English

In a linear order, the set s minus the union of all open intervals Ioo between pairs of elements of s is finite.

Русский

В линейном порядке множество меньше объединения всех открытых интервалов Ioo между парами элементов s по сути конечно.

LaTeX

$$$\\bigl(s \\setminus \\bigcup_{x \\in s,\, y \\in s} Ioo(x,y)\\bigr).Finite$$$

Lean4

theorem finite_diff_iUnion_Ioo (s : Set α) : (s \ ⋃ (x ∈ s) (y ∈ s), Ioo x y).Finite :=
  Set.finite_of_forall_not_lt_lt fun _x hx _y hy _z hz hxy hyz =>
    hy.2 <| mem_iUnion₂_of_mem hx.1 <| mem_iUnion₂_of_mem hz.1 ⟨hxy, hyz⟩

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