English
A well-founded linear order with a bottom yields a ConditionallyCompleteLinearOrderBot structure.
Русский
Нутажно-обоснованный линейный порядок с минимальным элементом образует структуру ConditionallyCompleteLinearOrderBot.
LaTeX
$$$\text{WellFoundedLT}.conditionallyCompleteLinearOrderBot (\alpha)$$$
Lean4
/-- A well-founded linear order is conditionally complete, with a bottom element. -/
noncomputable abbrev conditionallyCompleteLinearOrderBot (α : Type*) [i₁ : LinearOrder α] [i₂ : OrderBot α]
[h : WellFoundedLT α] : ConditionallyCompleteLinearOrderBot α :=
{ i₁, i₂,
LinearOrder.toLattice with
sInf := fun s => if hs : s.Nonempty then h.wf.min s hs else ⊥
csInf_le := fun s a _ has => by
have s_ne : s.Nonempty := ⟨a, has⟩
simpa [s_ne] using not_lt.1 (h.wf.not_lt_min s s_ne has)
le_csInf := fun s a hs has => by
simp only [hs, dif_pos]
exact has (h.wf.min_mem s hs)
sSup := fun s => if hs : (upperBounds s).Nonempty then h.wf.min _ hs else ⊥
le_csSup := fun s a hs has => by
have h's : (upperBounds s).Nonempty := hs
simp only [h's, dif_pos]
exact h.wf.min_mem _ h's has
csSup_le := fun s a _ has => by
have h's : (upperBounds s).Nonempty := ⟨a, has⟩
simp only [h's, dif_pos]
simpa using h.wf.not_lt_min _ h's has
csSup_empty := by simpa using eq_bot_iff.2 (not_lt.1 <| h.wf.not_lt_min _ _ <| mem_univ ⊥)
csSup_of_not_bddAbove := by
intro s H
have B : ¬((upperBounds s).Nonempty) := H
simp only [B, dite_false, upperBounds_empty, univ_nonempty, dite_true]
exact le_antisymm bot_le (WellFounded.min_le _ (mem_univ _))
csInf_of_not_bddBelow := fun s H ↦ (H (OrderBot.bddBelow s)).elim }
