lean_workbook_plus_27728
ProvedLet and let be real-valued functions such that for all in an open interval containing (but not necessarily at itself). If , then as well.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_27728 (a : ℝ) (f g h : ℝ → ℝ) (hf : ∀ x, f x ≤ g x) (hg : ∀ x, g x ≤ h x) (h1 : ContinuousAt f a) (h2 : ContinuousAt h a) (h3 : f a = h a) : ContinuousAt g a := by sorry
Source