Conditionally complete linear order structure on ℕ

In this file we

• define a ConditionallyCcompleteLinearOrderBot structure on ℕ;
• prove a few lemmas about supᵢ/infᵢ/Set.unionᵢ/Set.interᵢ and natural numbers.

ink

noncomputable instance Nat.instInfSetNat : InfSet ℕ

Equations

• Nat.instInfSetNat = { infₛ := fun s => if h : ∃ n, n ∈ s then Nat.find h else 0 }

ink

noncomputable instance Nat.instSupSetNat : SupSet ℕ

Equations

• Nat.instSupSetNat = { supₛ := fun s => if h : ∃ n, ∀ (a : ℕ), a ∈ s → a ≤ n then Nat.find h else 0 }

ink

theorem Nat.infₛ_def {s : Set ℕ} (h : Set.Nonempty s) : infₛ s = Nat.find h

ink

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

ink

theorem Nat.Set.Infinite.Nat.supₛ_eq_zero {s : Set ℕ} (h : Set.Infinite s) : supₛ s = 0

ink

@[simp]

theorem Nat.infₛ_eq_zero {s : Set ℕ} : infₛ s = 0 ↔ 0 ∈ s ∨ s = ∅

ink

@[simp]

theorem Nat.infₛ_empty : infₛ ∅ = 0

ink

@[simp]

theorem Nat.infᵢ_of_empty {ι : Sort u_1} [inst : IsEmpty ι] (f : ι → ℕ) : infᵢ f = 0

ink

theorem Nat.infₛ_mem {s : Set ℕ} (h : Set.Nonempty s) : infₛ s ∈ s

ink

theorem Nat.not_mem_of_lt_infₛ {s : Set ℕ} {m : ℕ} (hm : m < infₛ s) : ¬m ∈ s

ink

theorem Nat.infₛ_le {s : Set ℕ} {m : ℕ} (hm : m ∈ s) : infₛ s ≤ m

ink

theorem Nat.nonempty_of_pos_infₛ {s : Set ℕ} (h : 0 < infₛ s) : Set.Nonempty s

ink

theorem Nat.nonempty_of_infₛ_eq_succ {s : Set ℕ} {k : ℕ} (h : infₛ s = k + 1) : Set.Nonempty s

ink

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 (infₛ s)

ink

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

ink

instance Nat.instLatticeNat : Lattice ℕ

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

Equations

• Nat.instLatticeNat = LinearOrder.toLattice

ink

noncomputable instance Nat.instConditionallyCompleteLinearOrderBotNat : ConditionallyCompleteLinearOrderBot ℕ

Equations

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

ink

theorem Nat.supₛ_mem {s : Set ℕ} (h₁ : Set.Nonempty s) (h₂ : BddAbove s) : supₛ s ∈ s

ink

theorem Nat.infₛ_add {n : ℕ} {p : ℕ → Prop} (hn : n ≤ infₛ { m | p m }) : infₛ { m | p (m + n) } + n = infₛ { m | p m }

ink

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

ink

theorem Nat.supᵢ_lt_succ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ) : (⨆ k, ⨆ h, u k) = (⨆ k, ⨆ h, u k) ⊔ u n

ink

theorem Nat.supᵢ_lt_succ' {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ) : (⨆ k, ⨆ h, u k) = u 0 ⊔ ⨆ k, ⨆ h, u (k + 1)

ink

theorem Nat.infᵢ_lt_succ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ) : (⨅ k, ⨅ h, u k) = (⨅ k, ⨅ h, u k) ⊓ u n

ink

theorem Nat.infᵢ_lt_succ' {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ) : (⨅ k, ⨅ h, u k) = u 0 ⊓ ⨅ k, ⨅ h, u (k + 1)

ink

theorem Set.bunionᵢ_lt_succ {α : Type u_1} (u : ℕ → Set α) (n : ℕ) : (Set.unionᵢ fun k => Set.unionᵢ fun h => u k) = (Set.unionᵢ fun k => Set.unionᵢ fun h => u k) ∪ u n

ink

theorem Set.bunionᵢ_lt_succ' {α : Type u_1} (u : ℕ → Set α) (n : ℕ) : (Set.unionᵢ fun k => Set.unionᵢ fun h => u k) = u 0 ∪ Set.unionᵢ fun k => Set.unionᵢ fun h => u (k + 1)

ink

theorem Set.binterᵢ_lt_succ {α : Type u_1} (u : ℕ → Set α) (n : ℕ) : (Set.interᵢ fun k => Set.interᵢ fun h => u k) = (Set.interᵢ fun k => Set.interᵢ fun h => u k) ∩ u n

ink

theorem Set.binterᵢ_lt_succ' {α : Type u_1} (u : ℕ → Set α) (n : ℕ) : (Set.interᵢ fun k => Set.interᵢ fun h => u k) = u 0 ∩ Set.interᵢ fun k => Set.interᵢ fun h => u (k + 1)