English
In a dense, conditionally complete linear order, the set of all preconnected subsets equals the union of all intervals Icc, Ico, Ioc, Ioo, Ici, Ioi, Iic, Iio, together with ∅ and the whole space.
Русский
В плотной условиях полноты линейного порядка все предсвязные подмножества образуют союз всех интервалов Icc, Ico, Ioc, Ioo, Ici, Ioi, Iic, Iio, а также ∅ и всё пространство.
LaTeX
$${s : Set α | IsPreconnected s} = \\operatorname{range}(\\mathrm{uncurry} Icc) \\cup \\operatorname{range}(\\mathrm{uncurry} Ico) \\cup \\operatorname{range}(\\mathrm{uncurry} Ioc) \\cup \\operatorname{range}(\\mathrm{uncurry} Ioo) \\cup (\\operatorname{range} Ici ∪ \\operatorname{range} Ioi ∪ \\operatorname{range} Iic ∪ \\operatorname{range} Iio ∪ {univ, ∅})$$
Lean4
/-- In a dense conditionally complete linear order, the set of preconnected sets is exactly
the set of the intervals `Icc`, `Ico`, `Ioc`, `Ioo`, `Ici`, `Ioi`, `Iic`, `Iio`, `(-∞, +∞)`,
or `∅`. Though one can represent `∅` as `(sInf s, sInf s)`, we include it into the list of
possible cases to improve readability. -/
theorem setOf_isPreconnected_eq_of_ordered :
{s : Set α | IsPreconnected s} =
-- bounded intervals
range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
-- unbounded intervals and `univ`
(range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}) :=
by
refine Subset.antisymm setOf_isPreconnected_subset_of_ordered ?_
simp only [subset_def, forall_mem_range, uncurry, or_imp, forall_and, mem_union, mem_setOf_eq, insert_eq,
mem_singleton_iff, forall_eq, forall_true_iff, and_true, isPreconnected_Icc, isPreconnected_Ico, isPreconnected_Ioc,
isPreconnected_Ioo, isPreconnected_Ioi, isPreconnected_Iio, isPreconnected_Ici, isPreconnected_Iic,
isPreconnected_univ, isPreconnected_empty]
