proposition: Theorem alt_char_continuity : ∀ f : R → R, ∀ a : R, is_continuous_in f a ⇔ ∀ ε : R, ε > 0 ⇒ ∃ δ : R, (δ > 0) ∧ (∀ x : R, 0 < | x - a | < δ ⇒ | f(x) - f(a) | < ε).
proof: Proof. Take h : (R → R). Take a : R. We show both directions. * We need to show that (is_continuous_in(h, a) ⇒ for all ε : ℝ, ε > 0 ⇒ there exists δ : ℝ, δ > 0 ∧ (for all x : ℝ, 0 < |x - a| < δ ⇨ |h(x) - h(a)| < ε)). Assume that (is_continuous_in h a). Either ((is_accumulation_point a) ∧ (limit_in_point h a (h a))) or (is_isolated_point a). + Case ((is_accumulation_point a) ∧ (limit_in_point h a (h a))). Take ε : R. Assume that (ε > 0). It holds that (there exists δ1 : R, (δ1 > 0) ∧ (for all x : R, (0 < |x - a| < δ1) ⇒ (|(h x) - (h a)| < ε))). Obtain such a δ1. Choose δ := (δ1). We show both statements. - We conclude that (δ > 0). - We conclude that (for all x : ℝ, 0 < |x - a| < δ ⇨ |h(x) - h(a)| < ε). + Case (is_isolated_point a). It holds that (there exists ε : ℝ, ε > 0 ∧ (for all x : ℝ, |x - a| = 0 ∨ ε ≤ |x - a|)). Obtain such an ε. It holds that (ε > 0). Define z := (a + ε / 2). It holds that (|z - a| = 0 \/ ε ≤ | z - a |) (ii). destruct ii. - It holds that (| z - a | > 0). Contradiction. - It holds that (| z - a| < ε). Contradiction. * We need to show that ((for all ε : ℝ, ε > 0 ⇨ there exists δ : ℝ, δ > 0 ∧ (for all x : ℝ, 0 < |x - a| < δ ⇨ |h(x) - h(a)| < ε)) ⇨ is_continuous_in(h, a)). Assume that ((for all ε : ℝ, ε > 0 ⇨ there exists δ : ℝ, δ > 0 ∧ (for all x : ℝ, 0 < |x - a| < δ ⇨ |h(x) - h(a)| < ε))). unfold is_continuous_in. We need to show that (is_accumulation_point(a) ∧ limit_in_point(h, a, h(a)) ∨ is_isolated_point(a)). It suffices to show that (is_accumulation_point(a) ∧ limit_in_point(h, a, h(a)) ). We show both statements. + By (every_point_in_R_acc_point_R) we conclude that (is_accumulation_point a). + We conclude that (limit_in_point(h, a, h a)). Qed.
imports: Coq.Reals.Reals Notations Tactics Waterproof.Automation