mathlib3 documentation

data.nat.lattice

Conditionally complete linear order structure on ℕ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we

source
@[protected, instance]
noncomputable def nat.has_Inf  :
has_Inf ℕ
Equations
source
@[protected, instance]
noncomputable def nat.has_Sup  :
has_Sup ℕ
Equations
source
theorem nat.Inf_def {s : set ℕ} (h : s.nonempty) :
has_Inf.Inf s = nat.find h
source
theorem nat.Sup_def {s : set ℕ} (h : ∃ (n : ℕ), ∀ (a : ℕ), a ∈ s → a ≤ n) :
has_Sup.Sup s = nat.find h
source
theorem set.infinite.nat.Sup_eq_zero {s : set ℕ} (h : s.infinite) :
has_Sup.Sup s = 0
source
@[simp]
theorem nat.Inf_eq_zero {s : set ℕ} :
has_Inf.Inf s = 0 ↔ 0 ∈ s ∨ s = ∅
source
@[simp]
theorem nat.Inf_empty  :
has_Inf.Inf ∅ = 0
source
@[simp]
theorem nat.infi_of_empty {ι : Sort u_1} [is_empty ι] (f : ι → ℕ) :
infi f = 0
source
theorem nat.Inf_mem {s : set ℕ} (h : s.nonempty) :
has_Inf.Inf s ∈ s
source
theorem nat.not_mem_of_lt_Inf {s : set ℕ} {m : ℕ} (hm : m < has_Inf.Inf s) :
m ∉ s
source
@[protected]
theorem nat.Inf_le {s : set ℕ} {m : ℕ} (hm : m ∈ s) :
has_Inf.Inf s ≤ m
source
theorem nat.nonempty_of_pos_Inf {s : set ℕ} (h : 0 < has_Inf.Inf s) :
s.nonempty
source
theorem nat.nonempty_of_Inf_eq_succ {s : set ℕ} {k : ℕ} (h : has_Inf.Inf 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 (has_Inf.Inf s)
source
theorem nat.Inf_upward_closed_eq_succ_iff {s : set ℕ} (hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s) (k : ℕ) :
has_Inf.Inf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
source
@[protected, instance]
def nat.lattice  :
lattice ℕ

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

Equations
source
@[protected, instance]
noncomputable def nat.conditionally_complete_linear_order_bot  :
conditionally_complete_linear_order_bot ℕ
Equations
source
theorem nat.Sup_mem {s : set ℕ} (h₁ : s.nonempty) (h₂ : bdd_above s) :
has_Sup.Sup s ∈ s
source
theorem nat.Inf_add {n : ℕ} {p : ℕ → Prop} (hn : n ≤ has_Inf.Inf {m : ℕ | p m}) :
has_Inf.Inf {m : ℕ | p (m + n)} + n = has_Inf.Inf {m : ℕ | p m}
source
theorem nat.Inf_add' {n : ℕ} {p : ℕ → Prop} (h : 0 < has_Inf.Inf {m : ℕ | p m}) :
has_Inf.Inf {m : ℕ | p m} + n = has_Inf.Inf {m : ℕ | p (m - n)}
source
theorem nat.supr_lt_succ {α : Type u_1} [complete_lattice α] (u : ℕ → α) (n : ℕ) :
(⨆ (k : ℕ) (H : k < n + 1), u k) = (⨆ (k : ℕ) (H : k < n), u k) ⊔ u n
source
theorem nat.supr_lt_succ' {α : Type u_1} [complete_lattice α] (u : ℕ → α) (n : ℕ) :
(⨆ (k : ℕ) (H : k < n + 1), u k) = u 0 ⊔ ⨆ (k : ℕ) (H : k < n), u (k + 1)
source
theorem nat.infi_lt_succ {α : Type u_1} [complete_lattice α] (u : ℕ → α) (n : ℕ) :
(⨅ (k : ℕ) (H : k < n + 1), u k) = (⨅ (k : ℕ) (H : k < n), u k) ⊓ u n
source
theorem nat.infi_lt_succ' {α : Type u_1} [complete_lattice α] (u : ℕ → α) (n : ℕ) :
(⨅ (k : ℕ) (H : k < n + 1), u k) = u 0 ⊓ ⨅ (k : ℕ) (H : k < n), u (k + 1)
source
theorem set.bUnion_lt_succ {α : Type u_1} (u : ℕ → set α) (n : ℕ) :
(⋃ (k : ℕ) (H : k < n + 1), u k) = (⋃ (k : ℕ) (H : k < n), u k) ∪ u n
source
theorem set.bUnion_lt_succ' {α : Type u_1} (u : ℕ → set α) (n : ℕ) :
(⋃ (k : ℕ) (H : k < n + 1), u k) = u 0 ∪ ⋃ (k : ℕ) (H : k < n), u (k + 1)
source
theorem set.bInter_lt_succ {α : Type u_1} (u : ℕ → set α) (n : ℕ) :
(⋂ (k : ℕ) (H : k < n + 1), u k) = (⋂ (k : ℕ) (H : k < n), u k) ∩ u n
source
theorem set.bInter_lt_succ' {α : Type u_1} (u : ℕ → set α) (n : ℕ) :
(⋂ (k : ℕ) (H : k < n + 1), u k) = u 0 ∩ ⋂ (k : ℕ) (H : k < n), u (k + 1)