proposition: Lemma if_almost_maximizer_then_every_upp_bd_larger : ∀ (A : ℝ → Prop) (M : ℝ), (∀ (L : ℝ), L < M ⇒ ∃ a : ℝ, (A a) ∧ L < a) ⇒ ∀ (K : ℝ), is_upper_bound A K ⇒ M ≤ K.
proof: Proof. Take A : (ℝ → Prop) and M : ℝ. Assume that (∀ L : ℝ, L < M ⇒ there exists a : ℝ, (A a) ∧ L < a) (i). Take K : ℝ. Assume that (is_upper_bound A K). It holds that (∀ a : ℝ, (A a) ⇒ a ≤ K) (ii). We need to show that (M ≤ K). We argue by contradiction. Assume that (¬ M ≤ K). It holds that (M > K). By (i) it holds that (∃ a : ℝ, (A a) ∧ K < a). Obtain such an a. It holds that ((A a) ∧ (K < a)) (iii). Because (iii) both (A a) and (K < a) hold. By (ii) it holds that (a ≤ K). It holds that (K < K). It holds that (¬ (K < K)). Contradiction. Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics