Mathlib.Data.Nat.Lattice

Nat.instInfSet instance

: InfSet ℕ

Full source

noncomputable instance : InfSet ℕ :=
  ⟨fun s ↦ if h : ∃ n, n ∈ s then @Nat.find (fun n ↦ n ∈ s) _ h else 0⟩

Infimum Structure on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ have an `InfSet` structure, where for any nonempty subset $s \subseteq \mathbb{N}$, the infimum $\inf s$ is the smallest natural number in $s$.

Nat.instSupSet instance

: SupSet ℕ

Full source

noncomputable instance : SupSet ℕ :=
  ⟨fun s ↦ if h : ∃ n, ∀ a ∈ s, a ≤ n then @Nat.find (fun n ↦ ∀ a ∈ s, a ≤ n) _ h else 0⟩

Supremum Structure on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ have a supremum structure, where for any nonempty subset $s \subseteq \mathbb{N}$ that is bounded above, the supremum $\sup s$ is the smallest natural number that is an upper bound for all elements in $s$.

Nat.sInf_def theorem

{s : Set ℕ} (h : s.Nonempty) : sInf s = @Nat.find (fun n ↦ n ∈ s) _ h

Full source

theorem sInf_def {s : Set ℕ} (h : s.Nonempty) : sInf s = @Nat.find (fun n ↦ n ∈ s) _ h :=
  dif_pos _

Infimum of Nonempty Natural Number Set is its Minimal Element

Informal description

For any nonempty subset $s$ of natural numbers, the infimum $\inf s$ is equal to the smallest natural number $n$ such that $n \in s$.

Nat.sSup_def theorem

{s : Set ℕ} (h : ∃ n, ∀ a ∈ s, a ≤ n) : sSup s = @Nat.find (fun n ↦ ∀ a ∈ s, a ≤ n) _ h

Full source

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

Supremum of Bounded Natural Number Set is Minimal Upper Bound

Informal description

For any subset $s$ of natural numbers that is bounded above (i.e., there exists a natural number $n$ such that $a \leq n$ for all $a \in s$), the supremum $\sup s$ is equal to the smallest natural number $m$ satisfying $\forall a \in s, a \leq m$.

Set.Infinite.Nat.sSup_eq_zero theorem

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

Full source

theorem _root_.Set.Infinite.Nat.sSup_eq_zero {s : Set ℕ} (h : s.Infinite) : sSup s = 0 :=
  dif_neg fun ⟨n, hn⟩ ↦
    let ⟨k, hks, hk⟩ := h.exists_gt n
    (hn k hks).not_lt hk

Supremum of Infinite Natural Number Set is Zero

Informal description

For any infinite subset $s$ of natural numbers, the supremum of $s$ is equal to $0$, i.e., $\sup s = 0$.

Nat.sInf_eq_zero theorem

{s : Set ℕ} : sInf s = 0 ↔ 0 ∈ s ∨ s = ∅

Full source

@[simp]
theorem sInf_eq_zero {s : Set ℕ} : sInfsInf s = 0 ↔ 0 ∈ s ∨ s = ∅ := by
  cases eq_empty_or_nonempty s with
  | inl h => subst h
             simp only [or_true, eq_self_iff_true, iInf, InfSet.sInf,
                        mem_empty_iff_false, exists_false, dif_neg, not_false_iff]
  | inr h => simp only [h.ne_empty, or_false, Nat.sInf_def, h, Nat.find_eq_zero]

Infimum of Natural Number Set is Zero if and only if Zero is in the Set or the Set is Empty

Informal description

For any subset $s$ of natural numbers, the infimum $\inf s$ is equal to $0$ if and only if either $0$ is an element of $s$ or $s$ is the empty set.

Nat.sInf_empty theorem

: sInf ∅ = 0

Full source

@[simp]
theorem sInf_empty : sInf ∅ = 0 := by
  rw [sInf_eq_zero]
  right
  rfl

Infimum of Empty Set of Natural Numbers is Zero

Informal description

The infimum of the empty set of natural numbers is equal to $0$, i.e., $\inf \emptyset = 0$.

Nat.iInf_of_empty theorem

{ι : Sort*} [IsEmpty ι] (f : ι → ℕ) : iInf f = 0

Full source

@[simp]
theorem iInf_of_empty {ι : Sort*} [IsEmpty ι] (f : ι → ℕ) : iInf f = 0 := by
  rw [iInf_of_isEmpty, sInf_empty]

Infimum of Empty Indexed Family of Natural Numbers is Zero

Informal description

For any type `ι` that is empty and any function `f : ι → ℕ`, the infimum of `f` over `ι` is equal to 0, i.e., $\inf_{i \in \iota} f(i) = 0$.

Nat.iInf_const_zero theorem

{ι : Sort*} : ⨅ _ : ι, 0 = 0

Full source

/-- This combines `Nat.iInf_of_empty` with `ciInf_const`. -/
@[simp]
lemma iInf_const_zero {ι : Sort*} : ⨅ _ : ι, 0 = 0 :=
  (isEmpty_or_nonempty ι).elim (fun h ↦ by simp) fun h ↦ sInf_eq_zero.2 <| by simp

Infimum of Constant Zero Function is Zero

Informal description

For any type $\iota$, the infimum of the constant zero function over $\iota$ is equal to $0$, i.e., $\inf_{i \in \iota} 0 = 0$.

Nat.sInf_mem theorem

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

Full source

theorem sInf_mem {s : Set ℕ} (h : s.Nonempty) : sInfsInf s ∈ s := by
  classical
  rw [Nat.sInf_def h]
  exact Nat.find_spec h

Infimum of Nonempty Natural Number Set Belongs to the Set

Informal description

For any nonempty subset $s$ of natural numbers, the infimum $\inf s$ is an element of $s$.

Nat.not_mem_of_lt_sInf theorem

{s : Set ℕ} {m : ℕ} (hm : m < sInf s) : m ∉ s

Full source

theorem not_mem_of_lt_sInf {s : Set ℕ} {m : ℕ} (hm : m < sInf s) : m ∉ s := by
  classical
  cases eq_empty_or_nonempty s with
  | inl h => subst h; apply not_mem_empty
  | inr h => rw [Nat.sInf_def h] at hm; exact Nat.find_min h hm

Elements Below Infimum Are Not in the Set

Informal description

For any nonempty set $s$ of natural numbers and any natural number $m$, if $m$ is less than the infimum of $s$, then $m$ does not belong to $s$.

Nat.sInf_le theorem

{s : Set ℕ} {m : ℕ} (hm : m ∈ s) : sInf s ≤ m

Full source

protected theorem sInf_le {s : Set ℕ} {m : ℕ} (hm : m ∈ s) : sInf s ≤ m := by
  classical
  rw [Nat.sInf_def ⟨m, hm⟩]
  exact Nat.find_min' ⟨m, hm⟩ hm

Infimum of a Set of Natural Numbers is a Lower Bound

Informal description

For any nonempty subset $s$ of natural numbers and any natural number $m$ in $s$, the infimum of $s$ is less than or equal to $m$.

Nat.nonempty_of_pos_sInf theorem

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

Full source

theorem nonempty_of_pos_sInf {s : Set ℕ} (h : 0 < sInf s) : s.Nonempty := by
  by_contra contra
  rw [Set.not_nonempty_iff_eq_empty] at contra
  have h' : sInfsInf s ≠ 0 := ne_of_gt h
  apply h'
  rw [Nat.sInf_eq_zero]
  right
  assumption

Nonemptiness of Natural Number Set with Positive Infimum

Informal description

For any subset $s$ of natural numbers, if the infimum $\inf s$ is positive (i.e., $0 < \inf s$), then $s$ is nonempty.

Nat.nonempty_of_sInf_eq_succ theorem

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

Full source

theorem nonempty_of_sInf_eq_succ {s : Set ℕ} {k : ℕ} (h : sInf s = k + 1) : s.Nonempty :=
  nonempty_of_pos_sInf (h.symm ▸ succ_pos k : sInf s > 0)

Nonemptiness of Natural Number Set with Infimum Equal to Successor

Informal description

For any subset $s$ of natural numbers and any natural number $k$, if the infimum of $s$ equals $k + 1$, then $s$ is nonempty.

Nat.sInf_upward_closed_eq_succ_iff theorem

 {s : Set ℕ} (hs : ∀ k₁ k₂ : ℕ, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s) (k : ℕ) : sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Full source

theorem sInf_upward_closed_eq_succ_iff {s : Set ℕ} (hs : ∀ k₁ k₂ : ℕ, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s)
    (k : ℕ) : sInfsInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s := by
  classical
  constructor
  · intro H
    rw [eq_Ici_of_nonempty_of_upward_closed (nonempty_of_sInf_eq_succ _) hs, H, mem_Ici, mem_Ici]
    · exact ⟨le_rfl, k.not_succ_le_self⟩
    · exact k
    · assumption
  · rintro ⟨H, H'⟩
    rw [sInf_def (⟨_, H⟩ : s.Nonempty), find_eq_iff]
    exact ⟨H, fun n hnk hns ↦ H' <| hs n k (Nat.lt_succ_iff.mp hnk) hns⟩

Characterization of Infimum in Upward-Closed Sets of Natural Numbers: $\inf s = k + 1 \leftrightarrow (k + 1 \in s \land k \notin s)$

Informal description

For any subset $s$ of natural numbers that is upward-closed (i.e., if $k_1 \in s$ and $k_1 \leq k_2$, then $k_2 \in s$), and for any natural number $k$, the infimum of $s$ equals $k + 1$ if and only if $k + 1$ is in $s$ and $k$ is not in $s$.

Nat.instLattice instance

: Lattice ℕ

Full source

/-- This instance is necessary, otherwise the lattice operations would be derived via
`ConditionallyCompleteLinearOrderBot` and marked as noncomputable. -/
instance : Lattice ℕ :=
  LinearOrder.toLattice

The Lattice Structure on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ form a lattice with the usual order $\leq$, where the meet $\sqcap$ is the minimum and the join $\sqcup$ is the maximum of two numbers.

Nat.instConditionallyCompleteLinearOrderBot instance

: ConditionallyCompleteLinearOrderBot ℕ

Full source

noncomputable instance : ConditionallyCompleteLinearOrderBot ℕ :=
  { (inferInstance : OrderBot ℕ), (LinearOrder.toLattice : Lattice ℕ),
    (inferInstance : LinearOrder ℕ) with
    le_csSup := fun s a hb ha ↦ by rw [sSup_def hb]; revert a ha; exact @Nat.find_spec _ _ hb
    csSup_le := fun s a _ ha ↦ by rw [sSup_def ⟨a, ha⟩]; exact Nat.find_min' _ ha
    le_csInf := fun s a hs hb ↦ by
      rw [sInf_def hs]; exact hb (@Nat.find_spec (fun n ↦ n ∈ s) _ _)
    csInf_le := fun s a _ ha ↦ by rw [sInf_def ⟨a, ha⟩]; exact Nat.find_min' _ ha
    csSup_empty := by
      simp only [sSup_def, Set.mem_empty_iff_false, forall_const, forall_prop_of_false,
        not_false_iff, exists_const]
      apply bot_unique (Nat.find_min' _ _)
      trivial
    csSup_of_not_bddAbove := by
      intro s hs
      simp only [mem_univ, forall_true_left, sSup,
        mem_empty_iff_false, IsEmpty.forall_iff, forall_const, exists_const, dite_true]
      rw [dif_neg]
      · exact le_antisymm (zero_le _) (find_le trivial)
      · exact hs
    csInf_of_not_bddBelow := fun s hs ↦ by simp at hs }

Conditionally Complete Linear Order with Bottom on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ form a conditionally complete linear order with a bottom element, where every nonempty subset has an infimum and every nonempty bounded above subset has a supremum. The bottom element is $0$.

Nat.sSup_mem theorem

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

Full source

theorem sSup_mem {s : Set ℕ} (h₁ : s.Nonempty) (h₂ : BddAbove s) : sSupsSup s ∈ s :=
  let ⟨k, hk⟩ := h₂
  h₁.csSup_mem ((finite_le_nat k).subset hk)

Supremum of Bounded Nonempty Subset of Natural Numbers Belongs to the Subset

Informal description

For any nonempty subset $s$ of the natural numbers $\mathbb{N}$ that is bounded above, the supremum $\sup s$ is an element of $s$.

Nat.sInf_add theorem

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

Full source

theorem sInf_add {n : ℕ} {p : ℕ → Prop} (hn : n ≤ sInf { m | p m }) :
    sInf { m | p (m + n) } + n = sInf { m | p m } := by
  classical
  obtain h | ⟨m, hm⟩ := { m | p (m + n) }.eq_empty_or_nonempty
  · rw [h, Nat.sInf_empty, zero_add]
    obtain hnp | hnp := hn.eq_or_lt
    · exact hnp
    suffices hp : p (sInf { m | p m } - n + n) from (h.subset hp).elim
    rw [Nat.sub_add_cancel hn]
    exact csInf_mem (nonempty_of_pos_sInf <| n.zero_le.trans_lt hnp)
  · have hp : ∃ n, n ∈ { m | p m } := ⟨_, hm⟩
    rw [Nat.sInf_def ⟨m, hm⟩, Nat.sInf_def hp]
    rw [Nat.sInf_def hp] at hn
    exact find_add hn

Infimum Shift Identity for Natural Numbers

Informal description

For any natural number $n$ and predicate $p$ on natural numbers, if $n$ is less than or equal to the infimum of the set $\{m \mid p(m)\}$, then the infimum of the set $\{m \mid p(m + n)\}$ plus $n$ equals the infimum of $\{m \mid p(m)\}$. In other words, \[ \inf \{m \mid p(m + n)\} + n = \inf \{m \mid p(m)\}. \]

Nat.sInf_add' theorem

{n : ℕ} {p : ℕ → Prop} (h : 0 < sInf {m | p m}) : sInf {m | p m} + n = sInf {m | p (m - n)}

Full source

theorem sInf_add' {n : ℕ} {p : ℕ → Prop} (h : 0 < sInf { m | p m }) :
    sInf { m | p m } + n = sInf { m | p (m - n) } := by
  suffices h₁ : n ≤ sInf {m | p (m - n)} by
    convert sInf_add h₁
    simp_rw [Nat.add_sub_cancel_right]
  obtain ⟨m, hm⟩ := nonempty_of_pos_sInf h
  refine
    le_csInf ⟨m + n, ?_⟩ fun b hb ↦
      le_of_not_lt fun hbn ↦
        ne_of_mem_of_not_mem ?_ (not_mem_of_lt_sInf h) (Nat.sub_eq_zero_of_le hbn.le)
  · dsimp
    rwa [Nat.add_sub_cancel_right]
  · exact hb

Infimum Shift Identity for Natural Numbers (Subtractive Form)

Informal description

For any natural number $n$ and predicate $p$ on natural numbers, if the infimum of the set $\{m \mid p(m)\}$ is positive, then the sum of this infimum and $n$ equals the infimum of the set $\{m \mid p(m - n)\}$. In other words, \[ \inf \{m \mid p(m)\} + n = \inf \{m \mid p(m - n)\}. \]

Nat.iSup_lt_succ theorem

(u : ℕ → α) (n : ℕ) : ⨆ k < n + 1, u k = (⨆ k < n, u k) ⊔ u n

Full source

theorem iSup_lt_succ (u : ℕ → α) (n : ℕ) : ⨆ k < n + 1, u k = (⨆ k < n, u k) ⊔ u n := by
  simp_rw [Nat.lt_add_one_iff, biSup_le_eq_sup]

Supremum over Initial Segment of Natural Numbers with Successor

Informal description

For any sequence $u \colon \mathbb{N} \to \alpha$ and any natural number $n$, the supremum of $u$ over all $k < n + 1$ is equal to the supremum of $u$ over all $k < n$ joined with $u(n)$. That is, \[ \bigsqcup_{k < n + 1} u(k) = \left(\bigsqcup_{k < n} u(k)\right) \sqcup u(n). \]

Nat.iSup_lt_succ' theorem

(u : ℕ → α) (n : ℕ) : ⨆ k < n + 1, u k = u 0 ⊔ ⨆ k < n, u (k + 1)

Full source

theorem iSup_lt_succ' (u : ℕ → α) (n : ℕ) : ⨆ k < n + 1, u k = u 0 ⊔ ⨆ k < n, u (k + 1) := by
  rw [← sup_iSup_nat_succ]
  simp

Supremum over Initial Segment of Natural Numbers with Successor (Alternative Form)

Informal description

For any sequence $u \colon \mathbb{N} \to \alpha$ and any natural number $n$, the supremum of $u$ over all $k < n + 1$ is equal to the supremum of $u(0)$ and the supremum of $u(k+1)$ over all $k < n$. That is, \[ \bigsqcup_{k < n + 1} u(k) = u(0) \sqcup \left(\bigsqcup_{k < n} u(k+1)\right). \]

Nat.iInf_lt_succ theorem

(u : ℕ → α) (n : ℕ) : ⨅ k < n + 1, u k = (⨅ k < n, u k) ⊓ u n

Full source

theorem iInf_lt_succ (u : ℕ → α) (n : ℕ) : ⨅ k < n + 1, u k = (⨅ k < n, u k) ⊓ u n :=
  @iSup_lt_succ αᵒᵈ _ _ _

Infimum over Initial Segment of Natural Numbers with Successor

Informal description

For any sequence $u \colon \mathbb{N} \to \alpha$ and any natural number $n$, the infimum of $u$ over all $k < n + 1$ is equal to the infimum of $u$ over all $k < n$ meet $u(n)$. That is, \[ \bigsqcap_{k < n + 1} u(k) = \left(\bigsqcap_{k < n} u(k)\right) \sqcap u(n). \]

Nat.iInf_lt_succ' theorem

(u : ℕ → α) (n : ℕ) : ⨅ k < n + 1, u k = u 0 ⊓ ⨅ k < n, u (k + 1)

Full source

theorem iInf_lt_succ' (u : ℕ → α) (n : ℕ) : ⨅ k < n + 1, u k = u 0 ⊓ ⨅ k < n, u (k + 1) :=
  @iSup_lt_succ' αᵒᵈ _ _ _

Infimum over Initial Segment of Natural Numbers with Successor (Alternative Form)

Informal description

For any sequence $u \colon \mathbb{N} \to \alpha$ and any natural number $n$, the infimum of $u$ over all $k < n + 1$ is equal to the infimum of $u(0)$ and the infimum of $u(k+1)$ over all $k < n$. That is, \[ \bigsqcap_{k < n + 1} u(k) = u(0) \sqcap \left(\bigsqcap_{k < n} u(k+1)\right). \]

Nat.iSup_le_succ theorem

(u : ℕ → α) (n : ℕ) : ⨆ k ≤ n + 1, u k = (⨆ k ≤ n, u k) ⊔ u (n + 1)

Full source

theorem iSup_le_succ (u : ℕ → α) (n : ℕ) : ⨆ k ≤ n + 1, u k = (⨆ k ≤ n, u k) ⊔ u (n + 1) := by
  simp_rw [← Nat.lt_succ_iff, iSup_lt_succ]

Supremum over Initial Segment of Natural Numbers with Successor (Extended Form)

Informal description

For any sequence $u \colon \mathbb{N} \to \alpha$ and any natural number $n$, the supremum of $u$ over all $k \leq n + 1$ is equal to the supremum of $u$ over all $k \leq n$ joined with $u(n + 1)$. That is, \[ \bigsqcup_{k \leq n + 1} u(k) = \left(\bigsqcup_{k \leq n} u(k)\right) \sqcup u(n + 1). \]

Nat.iSup_le_succ' theorem

(u : ℕ → α) (n : ℕ) : ⨆ k ≤ n + 1, u k = u 0 ⊔ ⨆ k ≤ n, u (k + 1)

Full source

theorem iSup_le_succ' (u : ℕ → α) (n : ℕ) : ⨆ k ≤ n + 1, u k = u 0 ⊔ ⨆ k ≤ n, u (k + 1) := by
  simp_rw [← Nat.lt_succ_iff, iSup_lt_succ']

Supremum over Initial Segment of Natural Numbers with Successor (Extended Form)

Informal description

For any sequence $u \colon \mathbb{N} \to \alpha$ and any natural number $n$, the supremum of $u$ over all $k \leq n + 1$ is equal to the supremum of $u(0)$ and the supremum of $u(k+1)$ over all $k \leq n$. That is, \[ \sup_{k \leq n + 1} u(k) = u(0) \sqcup \left(\sup_{k \leq n} u(k+1)\right). \]

Nat.iInf_le_succ theorem

(u : ℕ → α) (n : ℕ) : ⨅ k ≤ n + 1, u k = (⨅ k ≤ n, u k) ⊓ u (n + 1)

Full source

theorem iInf_le_succ (u : ℕ → α) (n : ℕ) : ⨅ k ≤ n + 1, u k = (⨅ k ≤ n, u k) ⊓ u (n + 1) :=
  @iSup_le_succ αᵒᵈ _ _ _

Infimum over Initial Segment of Natural Numbers with Successor

Informal description

For any sequence $u \colon \mathbb{N} \to \alpha$ and any natural number $n$, the infimum of $u$ over all $k \leq n + 1$ is equal to the infimum of $u$ over all $k \leq n$ intersected with $u(n + 1)$. That is, \[ \bigsqcap_{k \leq n + 1} u(k) = \left(\bigsqcap_{k \leq n} u(k)\right) \sqcap u(n + 1). \]

Nat.iInf_le_succ' theorem

(u : ℕ → α) (n : ℕ) : ⨅ k ≤ n + 1, u k = u 0 ⊓ ⨅ k ≤ n, u (k + 1)

Full source

theorem iInf_le_succ' (u : ℕ → α) (n : ℕ) : ⨅ k ≤ n + 1, u k = u 0 ⊓ ⨅ k ≤ n, u (k + 1) :=
  @iSup_le_succ' αᵒᵈ _ _ _

Infimum Decomposition for Initial Segment of Natural Numbers with Successor (Alternative Form)

Informal description

For any sequence $u \colon \mathbb{N} \to \alpha$ and any natural number $n$, the infimum of $u(k)$ over all $k \leq n + 1$ is equal to the infimum of $u(0)$ and the infimum of $u(k+1)$ over all $k \leq n$. That is, \[ \inf_{k \leq n + 1} u(k) = u(0) \sqcap \left(\inf_{k \leq n} u(k+1)\right). \]

Set.biUnion_lt_succ theorem

(u : ℕ → Set α) (n : ℕ) : ⋃ k < n + 1, u k = (⋃ k < n, u k) ∪ u n

Full source

theorem biUnion_lt_succ (u : ℕ → Set α) (n : ℕ) : ⋃ k < n + 1, u k = (⋃ k < n, u k) ∪ u n :=
  Nat.iSup_lt_succ u n

Union of Sets over Initial Segment of Natural Numbers with Successor

Informal description

For any sequence of sets $u \colon \mathbb{N} \to \text{Set } \alpha$ and any natural number $n$, the union of $u(k)$ over all $k < n + 1$ is equal to the union of $u(k)$ over all $k < n$ combined with the set $u(n)$. That is, \[ \bigcup_{k < n + 1} u(k) = \left(\bigcup_{k < n} u(k)\right) \cup u(n). \]

Set.biUnion_lt_succ' theorem

(u : ℕ → Set α) (n : ℕ) : ⋃ k < n + 1, u k = u 0 ∪ ⋃ k < n, u (k + 1)

Full source

theorem biUnion_lt_succ' (u : ℕ → Set α) (n : ℕ) : ⋃ k < n + 1, u k = u 0 ∪ ⋃ k < n, u (k + 1) :=
  Nat.iSup_lt_succ' u n

Union Decomposition for Initial Segment of Natural Numbers with Successor (Alternative Form)

Informal description

For any sequence of sets $u \colon \mathbb{N} \to \text{Set } \alpha$ and any natural number $n$, the union of $u(k)$ over all $k < n + 1$ is equal to the union of $u(0)$ and the union of $u(k+1)$ over all $k < n$. That is, \[ \bigcup_{k < n + 1} u(k) = u(0) \cup \left(\bigcup_{k < n} u(k+1)\right). \]

Set.biInter_lt_succ theorem

(u : ℕ → Set α) (n : ℕ) : ⋂ k < n + 1, u k = (⋂ k < n, u k) ∩ u n

Full source

theorem biInter_lt_succ (u : ℕ → Set α) (n : ℕ) : ⋂ k < n + 1, u k = (⋂ k < n, u k) ∩ u n :=
  Nat.iInf_lt_succ u n

Intersection of Sets over Initial Segment of Natural Numbers with Successor

Informal description

For any sequence of sets $u \colon \mathbb{N} \to \text{Set } \alpha$ and any natural number $n$, the intersection of $u(k)$ over all $k < n + 1$ is equal to the intersection of $u(k)$ over all $k < n$ intersected with the set $u(n)$. That is, \[ \bigcap_{k < n + 1} u(k) = \left(\bigcap_{k < n} u(k)\right) \cap u(n). \]

Set.biInter_lt_succ' theorem

(u : ℕ → Set α) (n : ℕ) : ⋂ k < n + 1, u k = u 0 ∩ ⋂ k < n, u (k + 1)

Full source

theorem biInter_lt_succ' (u : ℕ → Set α) (n : ℕ) : ⋂ k < n + 1, u k = u 0 ∩ ⋂ k < n, u (k + 1) :=
  Nat.iInf_lt_succ' u n

Intersection Decomposition for Initial Segment of Natural Numbers with Successor (Alternative Form)

Informal description

For any sequence of sets $u \colon \mathbb{N} \to \text{Set } \alpha$ and any natural number $n$, the intersection of $u(k)$ over all $k < n + 1$ is equal to the intersection of $u(0)$ and the intersection of $u(k+1)$ over all $k < n$. That is, \[ \bigcap_{k < n + 1} u(k) = u(0) \cap \left(\bigcap_{k < n} u(k+1)\right). \]

Set.biUnion_le_succ theorem

(u : ℕ → Set α) (n : ℕ) : ⋃ k ≤ n + 1, u k = (⋃ k ≤ n, u k) ∪ u (n + 1)

Full source

theorem biUnion_le_succ (u : ℕ → Set α) (n : ℕ) : ⋃ k ≤ n + 1, u k = (⋃ k ≤ n, u k) ∪ u (n + 1) :=
  Nat.iSup_le_succ u n

Union of Sets over Initial Segment of Natural Numbers with Successor

Informal description

For any sequence of sets $u \colon \mathbb{N} \to \text{Set } \alpha$ and any natural number $n$, the union of $u(k)$ over all $k \leq n + 1$ is equal to the union of $u(k)$ over all $k \leq n$ combined with $u(n + 1)$. That is, \[ \bigcup_{k \leq n + 1} u(k) = \left(\bigcup_{k \leq n} u(k)\right) \cup u(n + 1). \]

Set.biUnion_le_succ' theorem

(u : ℕ → Set α) (n : ℕ) : ⋃ k ≤ n + 1, u k = u 0 ∪ ⋃ k ≤ n, u (k + 1)

Full source

theorem biUnion_le_succ' (u : ℕ → Set α) (n : ℕ) : ⋃ k ≤ n + 1, u k = u 0 ∪ ⋃ k ≤ n, u (k + 1) :=
  Nat.iSup_le_succ' u n

Union Decomposition for Initial Segment of Natural Numbers with Successor

Informal description

For any sequence of sets $u \colon \mathbb{N} \to \text{Set } \alpha$ and any natural number $n$, the union of $u(k)$ over all $k \leq n + 1$ is equal to the union of $u(0)$ and the union of $u(k+1)$ over all $k \leq n$. That is, \[ \bigcup_{k \leq n + 1} u(k) = u(0) \cup \left(\bigcup_{k \leq n} u(k+1)\right). \]

Set.biInter_le_succ theorem

(u : ℕ → Set α) (n : ℕ) : ⋂ k ≤ n + 1, u k = (⋂ k ≤ n, u k) ∩ u (n + 1)

Full source

theorem biInter_le_succ (u : ℕ → Set α) (n : ℕ) : ⋂ k ≤ n + 1, u k = (⋂ k ≤ n, u k) ∩ u (n + 1) :=
  Nat.iInf_le_succ u n

Intersection of Sets over Initial Segment of Natural Numbers with Successor

Informal description

For any sequence of sets $u \colon \mathbb{N} \to \text{Set } \alpha$ and any natural number $n$, the intersection of $u(k)$ over all $k \leq n + 1$ is equal to the intersection of $u(k)$ over all $k \leq n$ intersected with $u(n + 1)$. That is, \[ \bigcap_{k \leq n + 1} u(k) = \left(\bigcap_{k \leq n} u(k)\right) \cap u(n + 1). \]

Set.biInter_le_succ' theorem

(u : ℕ → Set α) (n : ℕ) : ⋂ k ≤ n + 1, u k = u 0 ∩ ⋂ k ≤ n, u (k + 1)

Full source

theorem biInter_le_succ' (u : ℕ → Set α) (n : ℕ) : ⋂ k ≤ n + 1, u k = u 0 ∩ ⋂ k ≤ n, u (k + 1) :=
  Nat.iInf_le_succ' u n

Intersection Decomposition for Initial Segment of Natural Numbers with Successor (Alternative Form)

Informal description

For any sequence of sets $u \colon \mathbb{N} \to \text{Set } \alpha$ and any natural number $n$, the intersection of $u(k)$ over all $k \leq n + 1$ is equal to the intersection of $u(0)$ and the intersection of $u(k+1)$ over all $k \leq n$. That is, \[ \bigcap_{k \leq n + 1} u(k) = u(0) \cap \left(\bigcap_{k \leq n} u(k+1)\right). \]

Set.accumulate_succ theorem

(u : ℕ → Set α) (n : ℕ) : Accumulate u (n + 1) = Accumulate u n ∪ u (n + 1)

Full source

theorem accumulate_succ (u : ℕ → Set α) (n : ℕ) :
    Accumulate u (n + 1) = AccumulateAccumulate u n ∪ u (n + 1) := biUnion_le_succ u n

Accumulation Step for Sets over Natural Numbers

Informal description

For any sequence of sets $u \colon \mathbb{N} \to \text{Set } \alpha$ and any natural number $n$, the accumulation of $u$ up to $n+1$ is equal to the accumulation of $u$ up to $n$ combined with $u(n + 1)$. That is, \[ \text{Accumulate } u (n + 1) = (\text{Accumulate } u n) \cup u(n + 1). \]