proposition: Lemma if_almost_maximizer_ε_then_every_upp_bd_larger : ∀ (A : ℝ → Prop) (M : ℝ), (∀ (ε : ℝ), ε > 0 ⇒ ∃ a : ℝ, (A a) ∧ M - ε < a) ⇒ ∀ (K : ℝ), is_upper_bound A K ⇒ M ≤ K.
proof: Proof. Take A : (ℝ → Prop) and M : ℝ. Assume that (for all ε : ℝ, ε > 0 ⇨ there exists a : ℝ, (A a) ∧ M - ε < a) (i). apply if_almost_maximizer_then_every_upp_bd_larger. Take L : ℝ; such that (L < M). It holds that (M - L > 0). Define ε1 := (M - L). 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). Because (ii) both (A a) and (M - ε1 < a) hold. Choose (a). We show both (A a) and (L < a). - We conclude that (A a). - We conclude that (& L = M - (M - L) = M - ε1 < a). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics