English
A connected subset that is bounded above and below contains the open interval between its infimum and supremum.
Русский
Связанное множество, ограниченное снизу и сверху, содержит открытый интервал между Inf и Sup.
LaTeX
$$$IsConnected(s) \land BddBelow(s) \land BddAbove(s) \Rightarrow Ioo(sInf(s), sSup(s)) \subseteq s$$$
Lean4
/-- A bounded connected subset of a conditionally complete linear order includes the open interval
`(Inf s, Sup s)`. -/
theorem Ioo_csInf_csSup_subset {s : Set α} (hs : IsConnected s) (hb : BddBelow s) (ha : BddAbove s) :
Ioo (sInf s) (sSup s) ⊆ s := fun _x hx =>
let ⟨_y, ys, hy⟩ := (isGLB_lt_iff (isGLB_csInf hs.nonempty hb)).1 hx.1
let ⟨_z, zs, hz⟩ := (lt_isLUB_iff (isLUB_csSup hs.nonempty ha)).1 hx.2
hs.Icc_subset ys zs ⟨hy.le, hz.le⟩