theorem stone_weierstrass (a b : ℝ) (hab : a ≤ b) (f : ℝ → ℝ) (hf : ContinuousOn f (Set.Icc a b)) (ε : ℝ) (hε : 0 < ε) : ∃ p : Polynomial ℝ, ∀ x ∈ Set.Icc a b, |f x - p.eval x| < ε := by have _ := hab let f_cont : C(Set.Icc a b, ℝ) := ⟨Set.restrict (Set.Icc a b...

theorem bolzano_weierstrass {s : Set ℝ} (h : Bornology.IsBounded s) (hs : s.Infinite) : ∃ x, AccPt x (Filter.principal s) := by have hK_closed : IsClosed (closure s) := isClosed_closure have hK_bounded ...

theorem heine_borel (s : Set ℝ) : IsCompact s ↔ IsClosed s ∧ Bornology.IsBounded s := Metric.isCompact_iff_isClosed_bounded

theorem banach_fixed {X : Type*} [MetricSpace X] [CompleteSpace X] [Nonempty X] {f : X → X} (hf : ContractingWith (1/2 : NNReal) f) : ∃! x, f x = x := by use ContractingWith.fixedPoint f hf constructor · show f (ContractingWith....

theorem brouwer_disc {n : ℕ} (f : Metric.closedBall (0 : EuclideanSpace ℝ (Fin n)) 1 → Metric.closedBall (0 : EuclideanSpace ℝ (Fin n)) 1) (hf : Continuous f) : ∃ x, f x = x := sorry

theorem pythag_thm (a b c : ℝ) (h : c = Real.sqrt (a ^ 2 + b ^ 2)) : a ^ 2 + b ^ 2 = c ^ 2 := by rw [h] symm apply Real.sq_sqrt positivity

theorem euclid_lemma (p a b : ℕ) (hp : p.Prime) (h : p ∣ a * b) : p ∣ a ∨ p ∣ b := hp.dvd_or_dvd h

theorem ivt {f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) (y : ℝ) (hy : y ∈ Set.Icc (f a) (f b)) : ∃ c ∈ Set.Icc a b, f c = y := intermediate_value_Icc hab hf hy

theorem mean_value_thm {f : ℝ → ℝ} {a b : ℝ} (hab : a < b) (hf : ContinuousOn f (Set.Icc a b)) (hf' : DifferentiableOn ℝ f (Set.Ioo a b)) : ∃ c ∈ Set.Ioo a b, deriv f c = (f b - f a) / (b - a) := exists_deriv_eq_slope f hab hf hf'

theorem inverse_function_thm {f : ℝ → ℝ} {a : ℝ} (hf : ContDiffAt ℝ 1 f a) (hf' : deriv f a ≠ 0) : ∃ g : ℝ → ℝ, ∃ U ∈ nhds a, ∀ x ∈ U, g (f x) = x ∧ f (g x) = x := sorry