mathlib documentation

data.nat.lattice

Conditionally complete linear order structure on #

In this file we

@[protected, instance]
noncomputable def nat.has_Inf  :
Equations
@[protected, instance]
noncomputable def nat.has_Sup  :
Equations
theorem nat.Inf_def {s : set } (h : s.nonempty) :
theorem nat.Sup_def {s : set } (h : ∃ (n : ), ∀ (a : ), a sa n) :
@[simp]
theorem nat.Inf_eq_zero {s : set } :
@[simp]
theorem nat.Inf_empty  :
@[simp]
theorem nat.infi_of_empty {ι : Sort u_1} [is_empty ι] (f : ι → ) :
infi f = 0
theorem nat.Inf_mem {s : set } (h : s.nonempty) :
theorem nat.not_mem_of_lt_Inf {s : set } {m : } (hm : m < has_Inf.Inf s) :
m s
@[protected]
theorem nat.Inf_le {s : set } {m : } (hm : m s) :
theorem nat.nonempty_of_pos_Inf {s : set } (h : 0 < has_Inf.Inf s) :
theorem nat.nonempty_of_Inf_eq_succ {s : set } {k : } (h : has_Inf.Inf s = k + 1) :
theorem nat.eq_Ici_of_nonempty_of_upward_closed {s : set } (hs : s.nonempty) (hs' : ∀ (k₁ k₂ : ), k₁ k₂k₁ sk₂ s) :
theorem nat.Inf_upward_closed_eq_succ_iff {s : set } (hs : ∀ (k₁ k₂ : ), k₁ k₂k₁ sk₂ s) (k : ) :
has_Inf.Inf s = k + 1 k + 1 s k s
@[protected, instance]

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

Equations
@[protected, instance]
Equations
theorem nat.Sup_mem {s : set } (h₁ : s.nonempty) (h₂ : bdd_above s) :
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}
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)}
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
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)
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
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)
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
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)
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
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)
@[protected, instance]
Equations