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