Documentation

Mathlib.Data.Int.ConditionallyCompleteOrder

forms a conditionally complete linear order #

The integers form a conditionally complete linear order.

Equations
  • One or more equations did not get rendered due to their size.
theorem Int.csupₛ_eq_greatest_of_bdd {s : Set } [inst : DecidablePred fun x => x s] (b : ) (Hb : ∀ (z : ), z sz b) (Hinh : z, z s) :
supₛ s = ↑(Int.greatestOfBdd b Hb Hinh)
theorem Int.cinfₛ_eq_least_of_bdd {s : Set } [inst : DecidablePred fun x => x s] (b : ) (Hb : ∀ (z : ), z sb z) (Hinh : z, z s) :
infₛ s = ↑(Int.leastOfBdd b Hb Hinh)
theorem Int.csupₛ_mem {s : Set } (h1 : Set.Nonempty s) (h2 : BddAbove s) :
theorem Int.cinfₛ_mem {s : Set } (h1 : Set.Nonempty s) (h2 : BddBelow s) :