English
If s is OrdConnected and t ⊆ s with t nonempty and bounded below, then the infimum of t lies in s.
Русский
Если s OrdConnected и t ⊆ s непусто и ограничено снизу, тогда инфиминум t лежит в s.
LaTeX
$$$$ t \neq \emptyset \land t \text{ bounded below } \Rightarrow \operatorname{sInf}(\operatorname{image} \operatorname{val} (t)) \in s $$$$
Lean4
/-- The `sInf` function on a nonempty `OrdConnected` set `s` in a conditionally complete linear
order takes values within `s`, for all nonempty bounded-below subsets of `s`. -/
theorem sInf_within_of_ordConnected {s : Set α} [hs : OrdConnected s] ⦃t : Set s⦄ (ht : t.Nonempty)
(h_bdd : BddBelow t) : sInf ((↑) '' t : Set α) ∈ s :=
by
obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht
obtain ⟨B, hB⟩ : ∃ B, B ∈ lowerBounds t := h_bdd
refine hs.out B.2 c.2 ⟨?_, ?_⟩
· exact (Subtype.mono_coe s).le_csInf_image ⟨c, hct⟩ hB
· exact (Subtype.mono_coe s).csInf_image_le hct ⟨B, hB⟩
