Documentation

Mathlib.Data.Nat.Lattice

Conditionally complete linear order structure on #

In this file we

noncomputable instance Nat.instInfSetNat :
Equations
noncomputable instance Nat.instSupSetNat :
Equations
theorem Nat.supₛ_def {s : Set } (h : n, ∀ (a : ), a sa n) :
@[simp]
theorem Nat.infₛ_eq_zero {s : Set } :
infₛ s = 0 0 s s =
@[simp]
theorem Nat.infᵢ_of_empty {ι : Sort u_1} [inst : IsEmpty ι] (f : ι) :
infᵢ f = 0
theorem Nat.not_mem_of_lt_infₛ {s : Set } {m : } (hm : m < infₛ s) :
¬m s
theorem Nat.infₛ_le {s : Set } {m : } (hm : m s) :
theorem Nat.eq_Ici_of_nonempty_of_upward_closed {s : Set } (hs : Set.Nonempty s) (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 : ) :
infₛ s = k + 1 k + 1 s ¬k s

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

Equations
Equations
  • One or more equations did not get rendered due to their size.
theorem Nat.supₛ_mem {s : Set } (h₁ : Set.Nonempty s) (h₂ : BddAbove s) :
theorem Nat.infₛ_add {n : } {p : Prop} (hn : n infₛ { m | p m }) :
infₛ { m | p (m + n) } + n = infₛ { m | p m }
theorem Nat.infₛ_add' {n : } {p : Prop} (h : 0 < infₛ { m | p m }) :
infₛ { m | p m } + n = infₛ { m | p (m - n) }
theorem Nat.supᵢ_lt_succ {α : Type u_1} [inst : CompleteLattice α] (u : α) (n : ) :
(k, h, u k) = (k, h, u k) u n
theorem Nat.supᵢ_lt_succ' {α : Type u_1} [inst : CompleteLattice α] (u : α) (n : ) :
(k, h, u k) = u 0 k, h, u (k + 1)
theorem Nat.infᵢ_lt_succ {α : Type u_1} [inst : CompleteLattice α] (u : α) (n : ) :
(k, h, u k) = (k, h, u k) u n
theorem Nat.infᵢ_lt_succ' {α : Type u_1} [inst : CompleteLattice α] (u : α) (n : ) :
(k, h, u k) = u 0 k, h, u (k + 1)
theorem Set.bunionᵢ_lt_succ {α : Type u_1} (u : Set α) (n : ) :
(Set.unionᵢ fun k => Set.unionᵢ fun h => u k) = (Set.unionᵢ fun k => Set.unionᵢ fun h => u k) u n
theorem Set.bunionᵢ_lt_succ' {α : Type u_1} (u : Set α) (n : ) :
(Set.unionᵢ fun k => Set.unionᵢ fun h => u k) = u 0 Set.unionᵢ fun k => Set.unionᵢ fun h => u (k + 1)
theorem Set.binterᵢ_lt_succ {α : Type u_1} (u : Set α) (n : ) :
(Set.interᵢ fun k => Set.interᵢ fun h => u k) = (Set.interᵢ fun k => Set.interᵢ fun h => u k) u n
theorem Set.binterᵢ_lt_succ' {α : Type u_1} (u : Set α) (n : ) :
(Set.interᵢ fun k => Set.interᵢ fun h => u k) = u 0 Set.interᵢ fun k => Set.interᵢ fun h => u (k + 1)