proposition: Theorem alt_char_continuity : ∀ f : ℕ → X, ∀ a : ℕ, is_continuous_in f a ⇔ ∀ ε : R, ε > 0 ⇒ ∃ δ : R, (δ > 0) ∧ (∀ x : ℕ, 0 < | x - a | < δ ⇒ dist X (f(x)) (f(a)) < ε).
proof: Proof. Take h : (ℕ → X). Take a : ℕ. 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| < δ ⇨ dist(X, h(x), h(a)) < ε)). Assume that (is_continuous_in h a). Take ε : R. Assume that (ε > 0). Choose δ := (1/2). We show both statements. - We conclude that (δ > 0). - We need to show that (for all x : nat, 0 < |x - a| < δ ⇨ dist(X, h(x), h(a)) < ε). Take x : nat. Assume that (0 < | x - a | < δ). Either (x = a) or (~(x=a)). + Case (x = a). It holds that (| x - a | = 0). Contradiction. + Case (~(x = a)). It holds that (1 ≤ | x - a |). Contradiction. * We need to show that ((for all ε : ℝ, ε > 0 ⇨ there exists δ : ℝ, δ > 0 ∧ (for all x : ℕ, 0 < |x - a| < δ ⇨ dist(X, h(x), h(a)) < ε)) ⇨ is_continuous_in(h, a)). Assume that ((for all ε : ℝ, ε > 0 ⇨ there exists δ : ℝ, δ > 0 ∧ (for all x : ℕ, 0 < |x - a| < δ ⇨ dist(X, h(x), h(a)) < ε))). 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_isolated_point a). unfold is_isolated_point. We need to show that (∃ ε : ℝ, ε > 0 ∧ (for all n : ℕ, |n - a| = 0 ∨ ε ≤ |n - a|)). Choose ε := (1/2). We show both statements. - We conclude that (ε > 0). - We need to show that (for all n : ℕ, |n - a| = 0 ∨ ε ≤ |n - a|). Take n : nat. Either (n = a) or (~(n=a)). + Case (n = a). It suffices to show that (|n - a| = 0). We conclude that (|n - a| = 0). + Case (~(n=a)). It suffices to show that ((1/2) ≤ | n - a |). It holds that (1 ≤ | n - a |). We conclude that (1/2 ≤ | n - a | ). Qed.
imports: Coq.Reals.Reals Tactics Automation Libs.Negation Notations