Documentation

Mathlib.Data.Nat.Lattice

Conditionally complete linear order structure on ℕ #

In this file we

source
noncomputable instance Nat.instInfSet :
InfSet ℕ
Equations
    source
    noncomputable instance Nat.instSupSet :
    SupSet ℕ
    Equations
      source
      theorem Nat.sInf_def {s : Set ℕ} (h : s.Nonempty) :
      sInf s = Nat.find h
      source
      theorem Nat.sSup_def {s : Set ℕ} (h : ∃ (n : ℕ), ∀ a ∈ s, a ≤ n) :
      sSup s = Nat.find h
      source
      theorem Set.Infinite.Nat.sSup_eq_zero {s : Set ℕ} (h : s.Infinite) :
      sSup s = 0
      source
      @[simp]
      theorem Nat.sInf_eq_zero {s : Set ℕ} :
      sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
      source
      @[simp]
      theorem Nat.sInf_empty :
      sInf ∅ = 0
      source
      @[simp]
      theorem Nat.iInf_of_empty {ι : Sort u_1} [IsEmpty ι] (f : ι → ℕ) :
      iInf f = 0
      source
      @[simp]
      theorem Nat.iInf_const_zero {ι : Sort u_1} :
      ⨅ (x : ι), 0 = 0

      This combines Nat.iInf_of_empty with ciInf_const.

      source
      theorem Nat.sInf_mem {s : Set ℕ} (h : s.Nonempty) :
      sInf s ∈ s
      source
      theorem Nat.notMem_of_lt_sInf {s : Set ℕ} {m : ℕ} (hm : m < sInf s) :
      m ∉ s
      source
      @[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.

      source
      theorem Nat.sInf_le {s : Set ℕ} {m : ℕ} (hm : m ∈ s) :
      sInf s ≤ m
      source
      theorem Nat.nonempty_of_pos_sInf {s : Set ℕ} (h : 0 < sInf s) :
      s.Nonempty
      source
      theorem Nat.nonempty_of_sInf_eq_succ {s : Set ℕ} {k : ℕ} (h : sInf s = k + 1) :
      s.Nonempty
      source
      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)
      source
      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
      source
      instance Nat.instLattice :
      Lattice ℕ

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

      Equations
        source
        noncomputable instance Nat.instConditionallyCompleteLinearOrderBot :
        ConditionallyCompleteLinearOrderBot ℕ
        Equations
          source
          theorem Nat.sSup_mem {s : Set ℕ} (h₁ : s.Nonempty) (h₂ : BddAbove s) :
          sSup s ∈ s
          source
          theorem Nat.sInf_add {n : ℕ} {p : ℕ → Prop} (hn : n ≤ sInf {m : ℕ | p m}) :
          sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}
          source
          theorem Nat.sInf_add' {n : ℕ} {p : ℕ → Prop} (h : 0 < sInf {m : ℕ | p m}) :
          sInf {m : ℕ | p m} + n = sInf {m : ℕ | p (m - n)}
          source
          theorem Nat.iSup_lt_succ {α : Type u_1} [CompleteLattice α] (u : ℕ → α) (n : ℕ) :
          ⨆ (k : ℕ), ⨆ (_ : k < n + 1), u k = (⨆ (k : ℕ), ⨆ (_ : k < n), u k) ⊔ u n
          source
          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)
          source
          theorem Nat.iInf_lt_succ {α : Type u_1} [CompleteLattice α] (u : ℕ → α) (n : ℕ) :
          ⨅ (k : ℕ), ⨅ (_ : k < n + 1), u k = (⨅ (k : ℕ), ⨅ (_ : k < n), u k) ⊓ u n
          source
          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)
          source
          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)
          source
          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)
          source
          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)
          source
          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)
          source
          theorem Set.biUnion_lt_succ {α : Type u_1} (u : ℕ → Set α) (n : ℕ) :
          ⋃ (k : ℕ), ⋃ (_ : k < n + 1), u k = (⋃ (k : ℕ), ⋃ (_ : k < n), u k) ∪ u n
          source
          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)
          source
          theorem Set.biInter_lt_succ {α : Type u_1} (u : ℕ → Set α) (n : ℕ) :
          ⋂ (k : ℕ), ⋂ (_ : k < n + 1), u k = (⋂ (k : ℕ), ⋂ (_ : k < n), u k) ∩ u n
          source
          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)
          source
          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)
          source
          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)
          source
          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)
          source
          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)
          source
          theorem Set.accumulate_succ {α : Type u_1} (u : ℕ → Set α) (n : ℕ) :
          Accumulate u (n + 1) = Accumulate u n ∪ u (n + 1)