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.instInfSetNat : InfSet ℕ

noncomputable instance Nat.instSupSetNat : SupSet ℕ

theorem Nat.sInf_def {s : Set ℕ} (h : Set.Nonempty s) : sInf s = Nat.find h

theorem Nat.sSup_def {s : Set ℕ} (h : ∃ n, ∀ (a : ℕ), a ∈ s → a ≤ n) : sSup s = Nat.find h

theorem Set.Infinite.Nat.sSup_eq_zero {s : Set ℕ} (h : Set.Infinite s) : sSup s = 0

@[simp]

theorem Nat.sInf_eq_zero {s : Set ℕ} : sInf s = 0 ↔ 0 ∈ s ∨ s = ∅

@[simp]

theorem Nat.sInf_empty : sInf ∅ = 0

@[simp]

theorem Nat.iInf_of_empty {ι : Sort u_1} [IsEmpty ι] (f : ι → ℕ) : iInf f = 0

theorem Nat.sInf_mem {s : Set ℕ} (h : Set.Nonempty s) : sInf s ∈ s

theorem Nat.not_mem_of_lt_sInf {s : Set ℕ} {m : ℕ} (hm : m < sInf s) : ¬m ∈ s

theorem Nat.sInf_le {s : Set ℕ} {m : ℕ} (hm : m ∈ s) : sInf s ≤ m

theorem Nat.nonempty_of_pos_sInf {s : Set ℕ} (h : 0 < sInf s) : Set.Nonempty s

theorem Nat.nonempty_of_sInf_eq_succ {s : Set ℕ} {k : ℕ} (h : sInf s = k + 1) : Set.Nonempty s

theorem Nat.eq_Ici_of_nonempty_of_upward_closed {s : Set ℕ} (hs : Set.Nonempty s) (hs' : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s) : s = Set.Ici (sInf s)

theorem Nat.sInf_upward_closed_eq_succ_iff {s : Set ℕ} (hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s) (k : ℕ) : sInf s = k + 1 ↔ k + 1 ∈ s ∧ ¬k ∈ s

instance Nat.instLatticeNat : Lattice ℕ

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

noncomputable instance Nat.instConditionallyCompleteLinearOrderBotNat : ConditionallyCompleteLinearOrderBot ℕ

theorem Nat.sSup_mem {s : Set ℕ} (h₁ : Set.Nonempty s) (h₂ : BddAbove s) : sSup s ∈ s

theorem Nat.sInf_add {n : ℕ} {p : ℕ → Prop} (hn : n ≤ sInf {m | p m}) : sInf {m | p (m + n)} + n = sInf {m | p m}

theorem Nat.sInf_add' {n : ℕ} {p : ℕ → Prop} (h : 0 < sInf {m | p m}) : sInf {m | p m} + n = sInf {m | p (m - n)}

theorem Nat.iSup_lt_succ {α : Type u_1} [CompleteLattice α] (u : ℕ → α) (n : ℕ) : ⨆ (k : ℕ) (_ : k < n + 1), u k = (⨆ (k : ℕ) (_ : k < n), u k) ⊔ u n

theorem Nat.iSup_lt_succ' {α : Type u_1} [CompleteLattice α] (u : ℕ → α) (n : ℕ) : ⨆ (k : ℕ) (_ : k < n + 1), u k = u 0 ⊔ ⨆ (k : ℕ) (_ : k < n), u (k + 1)

theorem Nat.iInf_lt_succ {α : Type u_1} [CompleteLattice α] (u : ℕ → α) (n : ℕ) : ⨅ (k : ℕ) (_ : k < n + 1), u k = (⨅ (k : ℕ) (_ : k < n), u k) ⊓ u n

theorem Nat.iInf_lt_succ' {α : Type u_1} [CompleteLattice α] (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)