proposition: Theorem alt_char_inf : ∀ (A : ℝ → Prop) (m : ℝ), is_inf A m ⇔ is_inf_alt_char A m.
proof: Proof. Take A : (ℝ → Prop) and m : ℝ. We show both directions. - We need to show that (is_inf A m ⇨ is_inf_alt_char A m). Assume that (is_inf A m). We need to show that ( is_lower_bound A m ∧ (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, (A a) ∧ m + ε > a) ). We show both statements. + We need to show that (is_lower_bound A m). It holds that ( is_lower_bound A m ∧ (for all l : ℝ, is_lower_bound A l ⇨ l ≤ m) ) (i). Because (i) both (is_lower_bound A m) and (for all l : ℝ, is_lower_bound A l ⇨ l ≤ m) hold. It follows that (is_lower_bound A m). + We need to show that (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, (A a) ∧ m + ε > a). By exists_almost_minimizer_ε we conclude that (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, (A a) ∧ m + ε > a). - We need to show that (is_inf_alt_char A m ⇨ is_inf A m). Assume that (is_inf_alt_char A m). It holds that ( is_lower_bound A m ∧ (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, (A a) ∧ m + ε > a) ) (i). Because (i) both (is_lower_bound A m) (ii) and (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, (A a) ∧ m + ε > a) hold. We need to show that ( is_lower_bound A m ∧ (for all l : ℝ, is_lower_bound A l ⇨ l ≤ m) ). We show both statements. + We need to show that (is_lower_bound A m). By (ii) we conclude that (is_lower_bound A m). + We need to show that (for all l : ℝ, is_lower_bound A l ⇨ l ≤ m). By if_almost_minimizer_ε_then_every_low_bd_smaller we conclude that (for all l : ℝ, is_lower_bound A l ⇨ l ≤ m). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics