proposition: Lemma exists_almost_minimizer : ∀ (A : ℝ → Prop) (m : ℝ), is_inf A m ⇒ ∀ (L : ℝ), L > m ⇒ ∃ a : ℝ, (A a) ∧ L > a.
proof: Proof. Take A : (ℝ → Prop). Take m : ℝ. Assume that (is_inf A m). Take L : ℝ. Assume that (L > m). We argue by contradiction. Assume that (¬ (there exists a : ℝ, (A a) ∧ L > a)). It holds that (∀ x : ℝ, (A x) ⇒ L ≤ x) (i). By (i) it holds that (is_lower_bound A L). By any_low_bd_le_inf it holds that (L <= m). It holds that (¬(L ≤ m)). Contradiction. Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics