theorem Real.volume_uIoc {a b : ℝ} : MeasureTheory.volume (Ι a b) = ENNReal.ofReal |b - a|

theorem intervalIntegral.integral_conj' {μ : MeasureTheory.Measure ℝ} {𝕜 : Type} [RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ} : ∫ (x : ℝ) in a..b, (starRingEnd 𝕜) (f x) ∂μ = (starRingEnd 𝕜) (∫ (x : ℝ) in a..b, f x ∂μ)

theorem intervalIntegrable_of_bdd {a b δ : ℝ} {g : ℝ → ℂ} (measurable_g : Measurable g) (bddg : ∀ (x : ℝ), ‖g x‖ ≤ δ) : IntervalIntegrable g MeasureTheory.volume a b

theorem IntervalIntegrable.bdd_mul {F : Type} [NormedDivisionRing F] {f g : ℝ → F} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hg : IntervalIntegrable g μ a b) (hm : MeasureTheory.AEStronglyMeasurable f μ) (hfbdd : ∃ (C : ℝ), ∀ (x : ℝ), ‖f x‖ ≤ C) : IntervalIntegrable (fun (x : ℝ) => f x * g x) μ a b

theorem IntervalIntegrable.mul_bdd {F : Type} [NormedField F] {f g : ℝ → F} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hf : IntervalIntegrable f μ a b) (hm : MeasureTheory.AEStronglyMeasurable g μ) (hgbdd : ∃ (C : ℝ), ∀ (x : ℝ), ‖g x‖ ≤ C) : IntervalIntegrable (fun (x : ℝ) => f x * g x) μ a b

theorem IntegrableOn.sub {α β : Type} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup β] {s : Set α} {f g : α → β} (hf : MeasureTheory.IntegrableOn f s μ) (hg : MeasureTheory.IntegrableOn g s μ) : MeasureTheory.IntegrableOn (f - g) s μ

theorem ConditionallyCompleteLattice.le_biSup {α : Type} [ConditionallyCompleteLinearOrder α] {ι : Type} [Nonempty ι] {f : ι → α} {s : Set ι} {a : α} (hfs : BddAbove (f '' s)) (ha : ∃ i ∈ s, f i = a) : a ≤ ⨆ i ∈ s, f i

theorem Function.Periodic.exists_mem_Ico₀' {α β : Type} {f : α → β} {c : α} [LinearOrderedAddCommGroup α] [Archimedean α] (h : Function.Periodic f c) (hc : 0 < c) (x : α) : ∃ (n : ℤ), x - n • c ∈ Set.Ico 0 c ∧ f x = f (x - n • c)

theorem Function.Periodic.exists_mem_Ico' {α β : Type} {f : α → β} {c : α} [LinearOrderedAddCommGroup α] [Archimedean α] (h : Function.Periodic f c) (hc : 0 < c) (x a : α) : ∃ (n : ℤ), x - n • c ∈ Set.Ico a (a + c) ∧ f x = f (x - n • c)