finite_diff_iUnion_Ioo' — Mathlib

English

For a linear order α and a set s, the same finiteness holds for the variant with a dependent union over s × s.

Русский

Для линейного порядка и множества s сохраняется конечность аналогично предыдущему утверждению с зависимым объединением по s × s.

LaTeX

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

Lean4

theorem finite_diff_iUnion_Ioo' (s : Set α) : (s \ ⋃ x : s × s, Ioo x.1 x.2).Finite := by
  simpa only [iUnion, iSup_prod, iSup_subtype] using s.finite_diff_iUnion_Ioo

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