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

• define a conditionally_complete_linear_order_bot structure on ℕ;
• prove a few lemmas about supr/infi/set.Union/set.Inter and natural numbers.
@[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 s a n) :
theorem set.infinite.nat.Sup_eq_zero {s : set } (h : s.infinite) :
= 0
@[simp]
theorem nat.Inf_eq_zero {s : set } :
= 0 0 s s =
@[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) :
s
theorem nat.not_mem_of_lt_Inf {s : set } {m : } (hm : m < ) :
m s
@[protected]
theorem nat.Inf_le {s : set } {m : } (hm : m s) :
m
theorem nat.nonempty_of_pos_Inf {s : set } (h : 0 < ) :
theorem nat.nonempty_of_Inf_eq_succ {s : set } {k : } (h : = k + 1) :
theorem nat.eq_Ici_of_nonempty_of_upward_closed {s : set } (hs : s.nonempty) (hs' : (k₁ k₂ : ), k₁ k₂ k₁ s k₂ s) :
s =
theorem nat.Inf_upward_closed_eq_succ_iff {s : set } (hs : (k₁ k₂ : ), k₁ k₂ k₁ s k₂ s) (k : ) :
= k + 1 k + 1 s k s
@[protected, instance]
def nat.lattice  :

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
• nat.conditionally_complete_linear_order_bot = {sup := , le := , lt := , le_refl := nat.conditionally_complete_linear_order_bot._proof_1, le_trans := nat.conditionally_complete_linear_order_bot._proof_2, lt_iff_le_not_le := nat.conditionally_complete_linear_order_bot._proof_3, le_antisymm := nat.conditionally_complete_linear_order_bot._proof_4, le_sup_left := nat.conditionally_complete_linear_order_bot._proof_5, le_sup_right := nat.conditionally_complete_linear_order_bot._proof_6, sup_le := nat.conditionally_complete_linear_order_bot._proof_7, inf := , inf_le_left := nat.conditionally_complete_linear_order_bot._proof_8, inf_le_right := nat.conditionally_complete_linear_order_bot._proof_9, le_inf := nat.conditionally_complete_linear_order_bot._proof_10, Sup := , Inf := , le_cSup := nat.conditionally_complete_linear_order_bot._proof_11, cSup_le := nat.conditionally_complete_linear_order_bot._proof_12, cInf_le := nat.conditionally_complete_linear_order_bot._proof_13, le_cInf := nat.conditionally_complete_linear_order_bot._proof_14, le_total := nat.conditionally_complete_linear_order_bot._proof_15, decidable_le := , decidable_eq := , decidable_lt := , max_def := nat.conditionally_complete_linear_order_bot._proof_16, min_def := nat.conditionally_complete_linear_order_bot._proof_17, bot := , bot_le := nat.conditionally_complete_linear_order_bot._proof_18, cSup_empty := nat.conditionally_complete_linear_order_bot._proof_19}
theorem nat.Sup_mem {s : set } (h₁ : s.nonempty) (h₂ : bdd_above s) :
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} (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} (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} (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} (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)