Ioo_csInf_csSup_subset — Mathlib

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⟩

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