Suprema_and_Infima_of_Combined_Bounded_Functions
Provedanalysisproofwiki
Let and be real functions. Let be a constant.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Suprema_and_Infima_of_Combined_Bounded_Functions (f g : ℝ → ℝ) (S : Set ℝ) (hS : S.Nonempty) (hfb : BddAbove (f '' S)) (hgb : BddAbove (g '' S)) : sSup ((fun x => f x + g x) '' S) ≤ sSup (f '' S) + sSup (g '' S) := by sorry
Source