proposition: Lemma if_almost_minimizer_then_every_low_bd_smaller : ∀ (A : ℝ → Prop) (m : ℝ), (∀ (L : ℝ), L > m ⇒ ∃ a : ℝ, (A a) ∧ L > a) ⇒ ∀ (K : ℝ), is_lower_bound A K ⇒ K ≤ m.
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_lower_bound A K). It holds that (∀ a : ℝ, (A a) ⇒ K ≤ a) (ii). We need to show that (K ≤ m). We argue by contradiction. Assume that (¬ K ≤ m). It holds that (K > m). 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 (K ≤ a). It holds that (K > K). It holds that (¬ (K > K)). Contradiction. Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics