proposition: Lemma sup_set_opp_is_inf_set : ∀ (A : ℝ → Prop) (M : ℝ), is_sup (set_opp A) M ⇒ is_inf A (-M).
proof: Proof. Take A : (ℝ → Prop) and M : ℝ. Assume that (is_sup (set_opp A) M). It holds that (is_upper_bound (set_opp A) M ∧ (for all M0 : ℝ, is_upper_bound (set_opp A) M0 ⇨ M ≤ M0)) (i). Because (i) both (is_upper_bound (set_opp A) M) and (for all M0 : ℝ, is_upper_bound (set_opp A) M0 ⇨ M ≤ M0) hold. We need to show that (is_lower_bound A (- M) ∧ (for all l : ℝ, is_lower_bound A l ⇨ l ≤ -M)). We show both statements. - We need to show that (is_lower_bound A (- M)). We claim that (is_upper_bound (set_opp A) M). We need to show that (for all a : ℝ, (set_opp A a) ⇒ a ≤ M). Take a : ℝ. Assume that (set_opp A a). It holds that (for all x : ℝ, (set_opp A x) ⇒ x ≤ M) (ii). By (ii) it holds that (is_upper_bound (set_opp A) M). We conclude that (a <= M). By upp_bd_set_opp_to_low_bd_set we conclude that (is_lower_bound A (-M)). - We need to show that (∀ l : ℝ, is_lower_bound A l ⇒ l ≤ -M). Take l : ℝ. Assume that (is_lower_bound A l). It holds that (is_upper_bound (set_opp A) M ∧ (for all M0 : ℝ, is_upper_bound (set_opp A) M0 ⇨ M ≤ M0)). It holds that (∀ b : ℝ, is_upper_bound (set_opp A) b ⇒ M ≤ b) (ii). By low_bd_set_to_upp_bd_set_opp it holds that (is_upper_bound (set_opp A) (-l)). By (ii) it holds that (M ≤ -l). We conclude that (l ≤ - M). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics