proposition: Theorem alt_char_sup : ∀ (A : ℝ → Prop) (M : ℝ), is_sup A M ⇔ is_sup_alt_char A M.
proof: Proof. Take A : (ℝ → Prop) and M : ℝ. We show both directions. - We need to show that (is_sup A M ⇨ is_sup_alt_char A M). Assume that (is_sup A M). We need to show that ( is_upper_bound A M ∧ (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, (A a) ∧ M - ε < a) ). We show both statements. + We need to show that (is_upper_bound A M). It holds that ( is_upper_bound A M ∧ (for all M0 : ℝ, is_upper_bound A M0 ⇨ M ≤ M0) ) (i). Because (i) both (is_upper_bound A M) and (for all M0 : ℝ, is_upper_bound A M0 ⇨ M ≤ M0) hold. It follows that (is_upper_bound A M). + We need to show that (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, (A a) ∧ M - ε < a ). apply exists_almost_maximizer_ε. We conclude that (M is the supremum of A). - We need to show that (is_sup_alt_char A M ⇨ is_sup A M). Assume that (is_sup_alt_char A M). It holds that ( is_upper_bound A M ∧ (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, (A a) ∧ M - ε < a) ) (i). Because (i) both (is_upper_bound A M) (ii) and (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, (A a) ∧ M - ε < a) (iii) hold. We need to show that ( is_upper_bound A M ∧ (for all M0 : ℝ, is_upper_bound A M0 ⇨ M ≤ M0) ). We show both statements. + We need to show that (is_upper_bound A M). By (ii) we conclude that (is_upper_bound A M). + We need to show that (for all M0 : ℝ, is_upper_bound A M0 ⇨ M ≤ M0). apply if_almost_maximizer_ε_then_every_upp_bd_larger. By (iii) we conclude that (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, A(a) ∧ M - ε < a). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics