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