def RealAnalysis.continuousAt (f : ℝ → ℝ) (x : ℝ) : Prop

Equations

• RealAnalysis.continuousAt f x = ∀ (ε : ℝ), 0 < ε → ∃ (δ : ℝ), 0 < δ ∧ ∀ (y : ℝ), |y - x| < δ → |f y - f x| < ε

def RealAnalysis.continuous (f : ℝ → ℝ) : Prop

Equations

• RealAnalysis.continuous f = ∀ (x : ℝ), RealAnalysis.continuousAt f x

theorem RealAnalysis.continuousAt_of_continuous {f : ℝ → ℝ} {x : ℝ} (h : continuous f) : continuousAt f x

theorem RealAnalysis.tendsTo_of_continuousAt {a : ℕ → ℝ} {f : ℝ → ℝ} {L : ℝ} (h₁ : tendsTo a L) (h₂ : continuousAt f L) : tendsTo (fun (x : ℕ) => f (a x)) (f L)

theorem RealAnalysis.tendsTo_of_continuous {a : ℕ → ℝ} {f : ℝ → ℝ} {L : ℝ} (h₁ : tendsTo a L) (h₂ : continuous f) : tendsTo (fun (x : ℕ) => f (a x)) (f L)

theorem RealAnalysis.continuous_exp : continuous fun (x : ℝ) => Real.exp x

theorem RealAnalysis.continuousAt_comp {f g : ℝ → ℝ} {x : ℝ} (hf : continuousAt f (g x)) (hg : continuousAt g x) : continuousAt (f ∘ g) x

theorem RealAnalysis.continuous_comp {f g : ℝ → ℝ} (hf : continuous f) (hg : continuous g) : continuous (f ∘ g)

theorem RealAnalysis.continuous_add_left {x : ℝ} : continuous fun (x_1 : ℝ) => x + x_1

theorem RealAnalysis.continuous_add_right {x : ℝ} : continuous fun (x_1 : ℝ) => x_1 + x

theorem RealAnalysis.continuous_neg : continuous fun (x : ℝ) => -x

theorem RealAnalysis.continuous_sub_left {x : ℝ} : continuous fun (x_1 : ℝ) => x - x_1

theorem RealAnalysis.continuous_sub_right {x : ℝ} : continuous fun (x_1 : ℝ) => x_1 - x

theorem RealAnalysis.continuous_mul_left {x : ℝ} : continuous fun (x_1 : ℝ) => x * x_1

theorem RealAnalysis.continuous_mul_right {x : ℝ} : continuous fun (x_1 : ℝ) => x_1 * x

theorem RealAnalysis.continuous_div_right {x : ℝ} : continuous fun (x_1 : ℝ) => x_1 / x

theorem RealAnalysis.continuous_rpow_left {b : ℝ} (hb : 0 < b) : continuous fun (x : ℝ) => b ^ x

theorem RealAnalysis.tendsTo_exp {a : ℕ → ℝ} {L : ℝ} (h : tendsTo a L) : tendsTo (fun (x : ℕ) => Real.exp (a x)) (Real.exp L)

theorem RealAnalysis.continuousAt_log {x : ℝ} (hx : 0 < x) : continuousAt (fun (x : ℝ) => Real.log x) x

theorem RealAnalysis.continuousAt_logb {b x : ℝ} (hx : 0 < x) : continuousAt (Real.logb b) x