English
Let α be a conditionally complete linear order. If s ⊆ α is nonempty and bounded below, and the infimum of s is not a predecessor-prelimit, then the infimum of s lies in s.
Русский
Пусть α — упорядоченный линейный порядок с условной полнотой. Если s ⊆ α непусто и ограничено снизу, иInf(s) не является пред-пределенным пределом, тогда Inf(s) принадлежит s.
LaTeX
$$$ \\forall \\alpha [ConditionallyCompleteLinearOrder \\alpha], \\forall s \\subseteq \\alpha,\; s \\neq \\varnothing \\to BddBelow(s) \\to \\neg IsPredPrelimit (sInf(s)) \\Rightarrow sInf(s) \\in s $$$
Lean4
theorem csInf_mem_of_not_isPredPrelimit (hne : s.Nonempty) (hbdd : BddBelow s) (hlim : ¬IsPredPrelimit (sInf s)) :
sInf s ∈ s := by
obtain ⟨y, hy⟩ := not_forall_not.mp hlim
obtain ⟨i, his, hi⟩ := exists_lt_of_csInf_lt hne hy.lt
exact eq_of_le_of_not_lt (csInf_le hbdd his) (hy.2 · hi) ▸ his
