conditionallyCompleteLinearOrder — Mathlib

English

If α is ConditionallyCompleteLinearOrder, then the upper set { x ∈ α : a ≤ x } is ConditionallyCompleteLinearOrder.

Русский

Если α имеет условно полную линейную упорядоченность, то верхнее множество { x ∈ α : a ≤ x } также образует условно полный линейный порядок.

LaTeX

$$$\\operatorname{ConditionallyCompleteLinearOrder}\\left\\{ x \\in \\alpha \\mid a \\le x \\right\\}$$$

Lean4

/-- If `sSup ∅ ≤ a` then `{x : α // a ≤ x}` is a `ConditionallyCompleteLinearOrder`. -/
protected noncomputable abbrev conditionallyCompleteLinearOrder [ConditionallyCompleteLinearOrder α] {a : α} :
    ConditionallyCompleteLinearOrder { x : α // a ≤ x } :=
  { @ordConnectedSubsetConditionallyCompleteLinearOrder α (Set.Ici a) _ ⟨⟨a, le_rfl⟩⟩ _ with }

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