The real numbers are an Archimedean floor ring, and a conditionally complete linear order.

instance Real.instArchimedean : Archimedean ℝ

Equations

• Real.instArchimedean = ⋯

noncomputable instance Real.instFloorRingRealInstLinearOrderedRingReal : FloorRing ℝ

Equations

• Real.instFloorRingRealInstLinearOrderedRingReal = Archimedean.floorRing ℝ

theorem Real.isCauSeq_iff_lift {f : ℕ → ℚ} : IsCauSeq abs f ↔ IsCauSeq abs fun (i : ℕ) => ↑(f i)

theorem Real.of_near (f : ℕ → ℚ) (x : ℝ) (h : ∀ ε > 0, ∃ (i : ℕ), ∀ j ≥ i, |↑(f j) - x| < ε) : ∃ (h' : IsCauSeq abs f), Real.mk { val := f, property := h' } = x

theorem Real.exists_floor (x : ℝ) : ∃ (ub : ℤ), ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub

theorem Real.exists_isLUB (S : Set ℝ) (hne : Set.Nonempty S) (hbdd : BddAbove S) : ∃ (x : ℝ), IsLUB S x

noncomputable instance Real.instSupSetReal : SupSet ℝ

Equations

• Real.instSupSetReal = { sSup := fun (S : Set ℝ) => if h : Set.Nonempty S ∧ BddAbove S then Classical.choose ⋯ else 0 }

theorem Real.sSup_def (S : Set ℝ) : sSup S = if h : Set.Nonempty S ∧ BddAbove S then Classical.choose ⋯ else 0

theorem Real.isLUB_sSup (S : Set ℝ) (h₁ : Set.Nonempty S) (h₂ : BddAbove S) : IsLUB S (sSup S)

noncomputable instance Real.instInfSetReal : InfSet ℝ

Equations

• Real.instInfSetReal = { sInf := fun (S : Set ℝ) => -sSup (-S) }

theorem Real.sInf_def (S : Set ℝ) : sInf S = -sSup (-S)

theorem Real.is_glb_sInf (S : Set ℝ) (h₁ : Set.Nonempty S) (h₂ : BddBelow S) : IsGLB S (sInf S)

noncomputable instance Real.instConditionallyCompleteLinearOrderReal : ConditionallyCompleteLinearOrder ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem Real.lt_sInf_add_pos {s : Set ℝ} (h : Set.Nonempty s) {ε : ℝ} (hε : 0 < ε) : ∃ a ∈ s, a < sInf s + ε

theorem Real.add_neg_lt_sSup {s : Set ℝ} (h : Set.Nonempty s) {ε : ℝ} (hε : ε < 0) : ∃ a ∈ s, sSup s + ε < a

theorem Real.sInf_le_iff {s : Set ℝ} (h : BddBelow s) (h' : Set.Nonempty s) {a : ℝ} : sInf s ≤ a ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε

theorem Real.le_sSup_iff {s : Set ℝ} (h : BddAbove s) (h' : Set.Nonempty s) {a : ℝ} : a ≤ sSup s ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x

@[simp]

theorem Real.sSup_empty : sSup ∅ = 0

@[simp]

theorem Real.iSup_of_isEmpty {α : Sort u_1} [IsEmpty α] (f : α → ℝ) : ⨆ (i : α), f i = 0

@[simp]

theorem Real.ciSup_const_zero {α : Sort u_1} : ⨆ (x : α), 0 = 0

theorem Real.sSup_of_not_bddAbove {s : Set ℝ} (hs : ¬BddAbove s) : sSup s = 0

theorem Real.iSup_of_not_bddAbove {α : Sort u_1} {f : α → ℝ} (hf : ¬BddAbove (Set.range f)) : ⨆ (i : α), f i = 0

theorem Real.sSup_univ : sSup Set.univ = 0

@[simp]

theorem Real.sInf_empty : sInf ∅ = 0

@[simp]

theorem Real.iInf_of_isEmpty {α : Sort u_1} [IsEmpty α] (f : α → ℝ) : ⨅ (i : α), f i = 0

@[simp]

theorem Real.ciInf_const_zero {α : Sort u_1} : ⨅ (x : α), 0 = 0

theorem Real.sInf_of_not_bddBelow {s : Set ℝ} (hs : ¬BddBelow s) : sInf s = 0

theorem Real.iInf_of_not_bddBelow {α : Sort u_1} {f : α → ℝ} (hf : ¬BddBelow (Set.range f)) : ⨅ (i : α), f i = 0

theorem Real.sSup_nonneg (S : Set ℝ) (hS : ∀ x ∈ S, 0 ≤ x) : 0 ≤ sSup S

As 0 is the default value for Real.sSup of the empty set or sets which are not bounded above, it suffices to show that S is bounded below by 0 to show that 0 ≤ sSup S.

theorem Real.iSup_nonneg {ι : Sort u_1} {f : ι → ℝ} (hf : ∀ (i : ι), 0 ≤ f i) : 0 ≤ ⨆ (i : ι), f i

As 0 is the default value for Real.sSup of the empty set or sets which are not bounded above, it suffices to show that f i is nonnegative to show that 0 ≤ ⨆ i, f i.

theorem Real.sSup_le {S : Set ℝ} {a : ℝ} (hS : ∀ x ∈ S, x ≤ a) (ha : 0 ≤ a) : sSup S ≤ a

As 0 is the default value for Real.sSup of the empty set or sets which are not bounded above, it suffices to show that all elements of S are bounded by a nonnegative number to show that sSup S is bounded by this number.

theorem Real.iSup_le {ι : Sort u_1} {f : ι → ℝ} {a : ℝ} (hS : ∀ (i : ι), f i ≤ a) (ha : 0 ≤ a) : ⨆ (i : ι), f i ≤ a

theorem Real.sSup_nonpos (S : Set ℝ) (hS : ∀ x ∈ S, x ≤ 0) : sSup S ≤ 0

As 0 is the default value for Real.sSup of the empty set, it suffices to show that S is bounded above by 0 to show that sSup S ≤ 0.

theorem Real.sInf_nonneg (S : Set ℝ) (hS : ∀ x ∈ S, 0 ≤ x) : 0 ≤ sInf S

As 0 is the default value for Real.sInf of the empty set, it suffices to show that S is bounded below by 0 to show that 0 ≤ sInf S.

theorem Real.iInf_nonneg {ι : Sort u_1} {f : ι → ℝ} (hf : ∀ (i : ι), 0 ≤ f i) : 0 ≤ iInf f

As 0 is the default value for Real.sInf of the empty set, it suffices to show that f i is bounded below by 0 to show that 0 ≤ iInf f.

theorem Real.sInf_nonpos (S : Set ℝ) (hS : ∀ x ∈ S, x ≤ 0) : sInf S ≤ 0

As 0 is the default value for Real.sInf of the empty set or sets which are not bounded below, it suffices to show that S is bounded above by 0 to show that sInf S ≤ 0.

theorem Real.sInf_le_sSup (s : Set ℝ) (h₁ : BddBelow s) (h₂ : BddAbove s) : sInf s ≤ sSup s

theorem Real.cauSeq_converges (f : CauSeq ℝ abs) : ∃ (x : ℝ), f ≈ CauSeq.const abs x

instance Real.instIsCompleteRealInstLinearOrderedFieldRealInstRingRealAbsLatticeInstAddGroupRealAbs_isAbsoluteValueInstLinearOrderedRingReal : CauSeq.IsComplete ℝ abs

Equations

• Real.instIsCompleteRealInstLinearOrderedFieldRealInstRingRealAbsLatticeInstAddGroupRealAbs_isAbsoluteValueInstLinearOrderedRingReal = ⋯

theorem Real.iInf_Ioi_eq_iInf_rat_gt {f : ℝ → ℝ} (x : ℝ) (hf : BddBelow (f '' Set.Ioi x)) (hf_mono : Monotone f) : ⨅ (r : ↑(Set.Ioi x)), f ↑r = ⨅ (q : { q' : ℚ // x < ↑q' }), f ↑↑q