theorem bddBelow_range_sub {α : Type u_1} {β : Type u_2} [LinearOrder β] [AddCommGroup β] [IsOrderedAddMonoid β] {a b : α → β} (ha : BddBelow (Set.range a)) (hb : BddAbove (Set.range b)) : BddBelow (Set.range (a - b))

theorem bddAbove_range_sub {α : Type u_1} {a b : α → ℝ} (ha : BddAbove (Set.range a)) (hb : BddBelow (Set.range b)) : BddAbove (Set.range (a - b))

theorem Pi.apply_single' {ι : Type u_1} {M : ι → Type u_2} {N : ι → Type u_3} [(i : ι) → Zero (M i)] [(i : ι) → Zero (N i)] [DecidableEq ι] {F : ι → Type u_4} [(i : ι) → FunLike (F i) (M i) (N i)] [∀ (i : ι), ZeroHomClass (F i) (M i) (N i)] (f' : (i : ι) → F i) (i : ι) (x : M i) (j : ι) : (f' j) (single i x j) = single i ((f' i) x) j

theorem Pi.intCast_single {ι : Type u_1} [DecidableEq ι] (a : ι) (b : ℤ) (x : ι) : ↑(single a b x) = single a (↑b) x

theorem Pi.single_mul_left_const_apply {ι : Type u_1} {α : Type u_2} [MulZeroClass α] [DecidableEq ι] (i j : ι) (a f : α) : single i (a * f) j = single i a j * f

theorem abs_sin_add_le (a b : ℝ) : |Real.sin (a + b)| ≤ |Real.sin a| + |Real.sin b|

theorem abs_sin_sum_le {ι : Type u_1} (s : Finset ι) (a : ι → ℝ) : |Real.sin (∑ i ∈ s, a i)| ≤ ∑ i ∈ s, |Real.sin (a i)|

theorem abs_sin_nat_mul_le (m : ℕ) (y : ℝ) : |Real.sin (↑m * y)| ≤ ↑m * |Real.sin y|

theorem sin_inequality {n : ℕ} (x : Fin n → ℤ) (y : Fin n → ℝ) : Real.sin (∑ i : Fin n, ↑(x i) * y i) ^ 2 ≤ (∑ k : Fin n, ↑(x k) ^ 2) * ∑ i : Fin n, Real.sin (y i) ^ 2

theorem integral_comp_polarCoord_symm_disk {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ × ℝ → E) : ∫ (p : ℝ × ℝ) in Set.Ioc 0 1 ×ˢ Set.Ioo (-Real.pi) Real.pi, p.1 • f (p.1 * Real.cos p.2, p.1 * Real.sin p.2) = ∫ (p : ℝ × ℝ) in {p : ℝ × ℝ | p.1 ^ 2 + p.2 ^ 2 ≤ 1}, f p

theorem two_mul_one_sub_cos_le (x : ℝ) : 2 * (1 - Real.cos x) ≤ x ^ 2

theorem one_sub_cos_le (x : ℝ) : 1 - Real.cos x ≤ x ^ 2 / 2

theorem cofinite_int_le_cobounded_real : Filter.map (fun (x : Fin 2 → ℤ) => (↑(x 0), ↑(x 1))) Filter.cofinite ≤ Bornology.cobounded (ℝ × ℝ)

theorem map_polarCoord_eq_cobounded : Filter.map (↑polarCoord.symm) (Filter.atTop ×ˢ Filter.principal (Set.Icc (-Real.pi) Real.pi)) = Bornology.cobounded (ℝ × ℝ)

theorem sin_cube_bound {x : ℝ} (hx : x ∈ Set.Icc (-1) 1) : |(x + Real.sin x) * (x - Real.sin x)| ≤ 2 * (Real.pi / 4) ^ 2 * (Real.sin x ^ 2 * x ^ 2)

theorem bounded_of_isBigO_cofinite {α : Type u_1} {f : α → ℝ} (hf : f =O[Filter.cofinite] 1) : ∃ (c : ℝ), ∀ (x : α), |f x| ≤ c