proposition: Lemma if_almost_minimizer_ε_then_every_low_bd_smaller : ∀ (A : ℝ → Prop) (m : ℝ), (∀ (ε : ℝ), ε > 0 ⇒ ∃ a : ℝ, (A a) ∧ m + ε > a) ⇒ ∀ (K : ℝ), is_lower_bound A K ⇒ K ≤ m.
proof: Proof. Take A : (ℝ → Prop) and m : ℝ. Assume that (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, (A a) ∧ m + ε > a) (i). apply if_almost_minimizer_then_every_low_bd_smaller. Take L : ℝ; such that (L > m). It holds that (L - m > 0). Define ε1 := (L - m). It holds that (ε1 > 0). By (i) it holds that (there exists a : ℝ, (A a) ∧ m + ε1 > a). Obtain such an a. It holds that ((A a) ∧ (m + ε1 > a)) (ii). Choose (a). Because (ii) both (A a) and (m + ε1 > a) hold. We show both (A a) and (L > a). - We conclude that (A a). - We conclude that (& a < m + ε1 = m + L - m = L). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics