instConditionallyCompleteLinearOrderBot

English

ℕ carries a ConditionallyComplete Linear Order with a bottom element 0.

Русский

Натуральные числа образуют условно-дополнительную линейную упорядоченность с основанием 0.

LaTeX

$$$\text{CCLOBot}(\mathbb{N})$$

Lean4

noncomputable instance : ConditionallyCompleteLinearOrderBot ℕ :=
  { (inferInstance : OrderBot ℕ), (LinearOrder.toLattice : Lattice ℕ),
    (inferInstance :
      LinearOrder
        ℕ) with
    le_csSup := fun s a hb ha ↦ by rw [sSup_def hb]; revert a ha; exact @Nat.find_spec _ _ hb
    csSup_le := fun s a _ ha ↦ by rw [sSup_def ⟨a, ha⟩]; exact Nat.find_min' _ ha
    le_csInf := fun s a hs hb ↦ by rw [sInf_def hs]; exact hb (@Nat.find_spec (fun n ↦ n ∈ s) _ _)
    csInf_le := fun s a _ ha ↦ by rw [sInf_def ⟨a, ha⟩]; exact Nat.find_min' _ ha
    csSup_empty :=
      by
      simp only [sSup_def, Set.mem_empty_iff_false, forall_const, forall_prop_of_false, not_false_iff, exists_const]
      apply bot_unique (Nat.find_min' _ _)
      trivial
    csSup_of_not_bddAbove := by
      intro s hs
      simp only [sSup, mem_empty_iff_false, IsEmpty.forall_iff, forall_const, exists_const, dite_true]
      rw [dif_neg]
      · exact le_antisymm (zero_le _) (find_le trivial)
      · exact hs
    csInf_of_not_bddBelow := fun s hs ↦ by simp at hs }

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