proposition: Lemma exists_inf : ∀ (A : ℝ → Prop) (x : ℝ), (A x) ⇒ is_bounded_below A ⇒ exists (m : ℝ), is_inf A m.
proof: Proof. Take A : (ℝ → Prop). Take z : ℝ. Assume that (A z). Assume that (is_bounded_below A) (vi). Define B := (set_opp A). We claim that (is_bounded_above B) (i). { By bdd_below_to_bdd_above_set_opp it suffices to show that (is_bounded_below A). We conclude that (is_bounded_below A). } We claim that (A (--z)). { It holds that (--z = z) (ii). It holds that (A z) (iii). exact (eq_ind_r(_,_,A,(iii),_,(ii))). } It holds that ((set_opp A) (-z)) (iv). It holds that (B (-z)). By R_complete it holds that (there exists M : ℝ, is_sup B M). Obtain such an M. Choose m := (- M). By sup_set_opp_is_inf_set we conclude that (is_inf A m). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics