English
A technical lemma: under suitable closedness and covering assumptions of Icc(a,b) by s,t, a nonempty intersection of Icc(a,b) with s∩t exists.
Русский
Техническая лема: при заданных условиях замкнутости и покрытия пересечение Icc(a,b) с s∩t непусто.
LaTeX
$$$(x,y, s,t)\text{ with } x,y\in Icc(a,b),\ Icc(a,b)\subseteq s\cup t \implies (Icc(a,b)\cap s\cap t)\neq\emptyset$$$
Lean4
/-- A preconnected set is either one of the intervals `Icc`, `Ico`, `Ioc`, `Ioo`, `Ici`, `Ioi`,
`Iic`, `Iio`, or `univ`, or `∅`. The converse statement requires `α` to be densely ordered. Though
one can represent `∅` as `(Inf ∅, Inf ∅)`, we include it into the list of possible cases to improve
readability. -/
theorem setOf_isPreconnected_subset_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
intro s hs
rcases hs.mem_intervals with (hs | hs | hs | hs | hs | hs | hs | hs | hs | hs) <;> rw [hs] <;>
simp only [union_insert, union_singleton, mem_insert_iff, mem_union, mem_range, Prod.exists, uncurry_apply_pair,
exists_apply_eq_apply, true_or, or_true, exists_apply_eq_apply2]
