Iio_csSup_subset — Mathlib

English

If s is preconnected, unbounded below, and bounded above, then all points below sSup(s) lie in s after excluding the supremum bound.

Русский

Если s предсоединено, не ограничено ниже и ограничено сверху, то все точки меньше sSup(s) принадлежат s.

LaTeX

$$$IsPreconnected(s) \land \neg BddBelow(s) \land BddAbove(s) \Rightarrow Iio(sSup(s)) \subseteq s$$$

Lean4

theorem Iio_csSup_subset {s : Set α} (hs : IsPreconnected s) (hb : ¬BddBelow s) (ha : BddAbove s) : Iio (sSup s) ⊆ s :=
  IsPreconnected.Ioi_csInf_subset (α := αᵒᵈ) hs ha hb

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