Supremum_Plus_Constant
Provedproofwikireal-analysis
Let be a subset of the set of real numbers . Let be bounded above. Let . Then where denotes supremum.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Supremum_Plus_Constant (S : Set ℝ) (hS : BddAbove S) (hne : S.Nonempty) (xi : ℝ) : sSup ((fun x => x + xi) '' S) = sSup S + xi := by sorry
Source