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

@[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) :
@[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₁ s k₂ s) :
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
@[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)