proposition: Lemma exists_almost_minimizer_ε : ∀ (A : ℝ → Prop) (m : ℝ), is_inf A m ⇒ ∀ (ε : ℝ), ε > 0 ⇒ ∃ a : ℝ, (A a) ∧ m + ε > a.
proof: Proof. Take A : (ℝ → Prop). Take m : ℝ. Assume that (is_inf A m). Take ε : ℝ; such that (ε > 0). It holds that (m + ε > m). apply exists_almost_minimizer with (L := m + ε) (m := m). - We conclude that (is_inf A m). - We conclude that (m + ε > m). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics