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

Equations

• Nat.instInfSet = { sInf := fun (s : Set ℕ) => if h : ∃ (n : ℕ), n ∈ s then Nat.find h else 0 }

noncomputable instance Nat.instSupSet : SupSet ℕ

Equations

• Nat.instSupSet = { sSup := fun (s : Set ℕ) => if h : ∃ (n : ℕ), ∀ a ∈ s, a ≤ n then Nat.find h else 0 }

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

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

theorem Set.Infinite.Nat.sSup_eq_zero {s : Set ℕ} (h : s.Infinite) : 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

@[simp]

theorem Nat.iInf_const_zero {ι : Sort u_1} : ⨅ (x : ι), 0 = 0

This combines Nat.iInf_of_empty with ciInf_const.

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

theorem Nat.notMem_of_lt_sInf {s : Set ℕ} {m : ℕ} (hm : m < sInf s) : m ∉ s

@[deprecated Nat.notMem_of_lt_sInf (since := "2025-05-23")]

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

Alias of Nat.notMem_of_lt_sInf.

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) : s.Nonempty

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

theorem Nat.eq_Ici_of_nonempty_of_upward_closed {s : Set ℕ} (hs : s.Nonempty) (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.instLattice : Lattice ℕ

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

Equations

• Nat.instLattice = LinearOrder.toLattice

noncomputable instance Nat.instConditionallyCompleteLinearOrderBot : ConditionallyCompleteLinearOrderBot ℕ

Equations

• One or more equations did not get rendered due to their size.

theorem Nat.sSup_mem {s : Set ℕ} (h₁ : s.Nonempty) (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 Nat.iSup_le_succ {α : Type u_1} [CompleteLattice α] (u : ℕ → α) (n : ℕ) : ⨆ (k : ℕ), ⨆ (_ : k ≤ n + 1), u k = (⨆ (k : ℕ), ⨆ (_ : k ≤ n), u k) ⊔ u (n + 1)

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

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

theorem Nat.iInf_le_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)

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)

theorem Set.accumulate_succ {α : Type u_1} (u : ℕ → Set α) (n : ℕ) : Accumulate u (n + 1) = Accumulate u n ∪ u (n + 1)