English
If α is ConditionallyCompleteLinearOrder, then the upper set { x ∈ α : a ≤ x } has a bottom element and is ConditionallyCompleteLinearOrderBot.
Русский
Если α — условно полная линейная упорядоченность, то верхнее множество { x ∈ α : a ≤ x } имеет нижний элемент и является ConditionallyCompleteLinearOrderBot.
LaTeX
$$$\\operatorname{ConditionallyCompleteLinearOrderBot}\\left\\{ x \\in \\alpha \\mid a \\le x \\right\\}$$$
Lean4
/-- If `sSup ∅ ≤ a` then `{x : α // a ≤ x}` is a `ConditionallyCompleteLinearOrderBot`.
This instance uses data fields from `Subtype.linearOrder` to help type-class inference.
The `Set.Ici` data fields are definitionally equal, but that requires unfolding semireducible
definitions, so type-class inference won't see this. -/
protected noncomputable abbrev conditionallyCompleteLinearOrderBot [ConditionallyCompleteLinearOrder α] (a : α) :
ConditionallyCompleteLinearOrderBot { x : α // a ≤ x } :=
{ Nonneg.orderBot, Nonneg.conditionallyCompleteLinearOrder with
csSup_empty := by rw [@subset_sSup_def α (Set.Ici a) _ _ ⟨⟨a, le_rfl⟩⟩]; simp [bot_eq] }
