# Conditionally complete linear order structure on ℕ#

In this file we

• define a ConditionallyCompleteLinearOrderBot structure on ℕ;
• prove a few lemmas about iSup/iInf/Set.iUnion/Set.iInter and natural numbers.
noncomputable instance Nat.instInfSet :
Equations
noncomputable instance Nat.instSupSet :
Equations
theorem Nat.sInf_def {s : } (h : s.Nonempty) :
sInf s =
theorem Nat.sSup_def {s : } (h : ∃ (n : ), as, a n) :
sSup s =
theorem Set.Infinite.Nat.sSup_eq_zero {s : } (h : s.Infinite) :
sSup s = 0
@[simp]
theorem Nat.sInf_eq_zero {s : } :
sInf s = 0 0 s s =
@[simp]
theorem Nat.sInf_empty :
= 0
@[simp]
theorem Nat.iInf_of_empty {ι : Sort u_1} [] (f : ι) :
iInf f = 0
@[simp]
theorem Nat.iInf_const_zero {ι : Sort u_1} :
⨅ (i : ι), 0 = 0

This combines Nat.iInf_of_empty with ciInf_const.

theorem Nat.sInf_mem {s : } (h : s.Nonempty) :
sInf s s
theorem Nat.not_mem_of_lt_sInf {s : } {m : } (hm : m < sInf s) :
ms
theorem Nat.sInf_le {s : } {m : } (hm : m s) :
sInf s m
theorem Nat.nonempty_of_pos_sInf {s : } (h : 0 < sInf s) :
s.Nonempty
theorem Nat.nonempty_of_sInf_eq_succ {s : } {k : } (h : sInf s = k + 1) :
s.Nonempty
theorem Nat.eq_Ici_of_nonempty_of_upward_closed {s : } (hs : s.Nonempty) (hs' : ∀ (k₁ k₂ : ), k₁ k₂k₁ sk₂ s) :
s = Set.Ici (sInf s)
theorem Nat.sInf_upward_closed_eq_succ_iff {s : } (hs : ∀ (k₁ k₂ : ), k₁ k₂k₁ sk₂ s) (k : ) :
sInf s = k + 1 k + 1 s ks
instance Nat.instLattice :

This instance is necessary, otherwise the lattice operations would be derived via ConditionallyCompleteLinearOrderBot and marked as noncomputable.

Equations
Equations
• One or more equations did not get rendered due to their size.
theorem Nat.sSup_mem {s : } (h₁ : s.Nonempty) (h₂ : ) :
sSup s s
theorem Nat.sInf_add {n : } {p : } (hn : n sInf {m : | p m}) :
sInf {m : | p (m + n)} + n = sInf {m : | p m}
theorem Nat.sInf_add' {n : } {p : } (h : 0 < sInf {m : | p m}) :
sInf {m : | p m} + n = sInf {m : | p (m - n)}
theorem Nat.iSup_lt_succ {α : Type u_1} [] (u : α) (n : ) :
⨆ (k : ), ⨆ (_ : k < n + 1), u k = (⨆ (k : ), ⨆ (_ : k < n), u k) u n
theorem Nat.iSup_lt_succ' {α : Type u_1} [] (u : α) (n : ) :
⨆ (k : ), ⨆ (_ : k < n + 1), u k = u 0 ⨆ (k : ), ⨆ (_ : k < n), u (k + 1)
theorem Nat.iInf_lt_succ {α : Type u_1} [] (u : α) (n : ) :
⨅ (k : ), ⨅ (_ : k < n + 1), u k = (⨅ (k : ), ⨅ (_ : k < n), u k) u n
theorem Nat.iInf_lt_succ' {α : Type u_1} [] (u : α) (n : ) :
⨅ (k : ), ⨅ (_ : k < n + 1), u k = u 0 ⨅ (k : ), ⨅ (_ : k < n), u (k + 1)
theorem Nat.iSup_le_succ {α : Type u_1} [] (u : α) (n : ) :
⨆ (k : ), ⨆ (_ : k n + 1), u k = (⨆ (k : ), ⨆ (_ : k n), u k) u (n + 1)
theorem Nat.iSup_le_succ' {α : Type u_1} [] (u : α) (n : ) :
⨆ (k : ), ⨆ (_ : k n + 1), u k = u 0 ⨆ (k : ), ⨆ (_ : k n), u (k + 1)
theorem Nat.iInf_le_succ {α : Type u_1} [] (u : α) (n : ) :
⨅ (k : ), ⨅ (_ : k n + 1), u k = (⨅ (k : ), ⨅ (_ : k n), u k) u (n + 1)
theorem Nat.iInf_le_succ' {α : Type u_1} [] (u : α) (n : ) :
⨅ (k : ), ⨅ (_ : k n + 1), u k = u 0 ⨅ (k : ), ⨅ (_ : k n), u (k + 1)
theorem Set.biUnion_lt_succ {α : Type u_1} (u : Set α) (n : ) :
⋃ (k : ), ⋃ (_ : k < n + 1), u k = (⋃ (k : ), ⋃ (_ : k < n), u k) u n
theorem Set.biUnion_lt_succ' {α : Type u_1} (u : Set α) (n : ) :
⋃ (k : ), ⋃ (_ : k < n + 1), u k = u 0 ⋃ (k : ), ⋃ (_ : k < n), u (k + 1)
theorem Set.biInter_lt_succ {α : Type u_1} (u : Set α) (n : ) :
⋂ (k : ), ⋂ (_ : k < n + 1), u k = (⋂ (k : ), ⋂ (_ : k < n), u k) u n
theorem Set.biInter_lt_succ' {α : Type u_1} (u : Set α) (n : ) :
⋂ (k : ), ⋂ (_ : k < n + 1), u k = u 0 ⋂ (k : ), ⋂ (_ : k < n), u (k + 1)
theorem Set.biUnion_le_succ {α : Type u_1} (u : Set α) (n : ) :
⋃ (k : ), ⋃ (_ : k n + 1), u k = (⋃ (k : ), ⋃ (_ : k n), u k) u (n + 1)
theorem Set.biUnion_le_succ' {α : Type u_1} (u : Set α) (n : ) :
⋃ (k : ), ⋃ (_ : k n + 1), u k = u 0 ⋃ (k : ), ⋃ (_ : k n), u (k + 1)
theorem Set.biInter_le_succ {α : Type u_1} (u : Set α) (n : ) :
⋂ (k : ), ⋂ (_ : k n + 1), u k = (⋂ (k : ), ⋂ (_ : k n), u k) u (n + 1)
theorem Set.biInter_le_succ' {α : Type u_1} (u : Set α) (n : ) :
⋂ (k : ), ⋂ (_ : k n + 1), u k = u 0 ⋂ (k : ), ⋂ (_ : k n), u (k + 1)