Documentation

Books.IntroductiontoRealAnalysisVolumeI_JiriLebl_2025.Chapters.Chap03.section06

def increasingOn (f : ) (S : Set ) :

Definition 3.6.1: Let S ⊆ ℝ. A function f : ℝ → ℝ is increasing (resp. strictly increasing) on S if x < y with x, y ∈ S implies f x ≤ f y (resp. f x < f y). It is decreasing (resp. strictly decreasing) when the inequalities for f are reversed. A function that is either increasing or decreasing on S is called monotone on S, and if it is strictly increasing or strictly decreasing on S, it is called strictly monotone on S.

Equations
Instances For
    def strictlyIncreasingOn (f : ) (S : Set ) :
    Equations
    Instances For
      def decreasingOn (f : ) (S : Set ) :
      Equations
      Instances For
        def strictlyDecreasingOn (f : ) (S : Set ) :
        Equations
        Instances For
          def monotoneOn (f : ) (S : Set ) :
          Equations
          Instances For
            theorem monotoneOn_left_limit_sup {S : Set } {f : } {c : } (hf : MonotoneOn f S) (hc : c closure (S Set.Iio c)) (hB : BddAbove (f '' (S Set.Iio c))) :

            A technical lemma: if f is monotone on S, then the left limit along S ∩ (-∞, c) converges to the supremum of the left slice when that slice is bounded above.

            theorem monotoneOn_left_limit_atTop {S : Set } {f : } {c : } (hf : MonotoneOn f S) (hc : c closure (S Set.Iio c)) (hUnb : ¬BddAbove (f '' (S Set.Iio c))) :
            theorem monotoneOn_right_limit_inf {S : Set } {f : } {c : } (hf : MonotoneOn f S) (hc : c closure (S Set.Ioi c)) (hB : BddBelow (f '' (S Set.Ioi c))) :
            theorem monotoneOn_right_limit_atBot {S : Set } {f : } {c : } (hf : MonotoneOn f S) (hc : c closure (S Set.Ioi c)) (hUnb : ¬BddBelow (f '' (S Set.Ioi c))) :
            theorem antitoneOn_left_limit_inf {S : Set } {g : } {c : } (hg : AntitoneOn g S) (hc : c closure (S Set.Iio c)) (hB : BddBelow (g '' (S Set.Iio c))) :
            theorem antitoneOn_left_limit_atBot {S : Set } {g : } {c : } (hg : AntitoneOn g S) (hc : c closure (S Set.Iio c)) (hUnb : ¬BddBelow (g '' (S Set.Iio c))) :
            theorem antitoneOn_right_limit_sup {S : Set } {g : } {c : } (hg : AntitoneOn g S) (hc : c closure (S Set.Ioi c)) (hB : BddAbove (g '' (S Set.Ioi c))) :
            theorem antitoneOn_right_limit_atTop {S : Set } {g : } {c : } (hg : AntitoneOn g S) (hc : c closure (S Set.Ioi c)) (hUnb : ¬BddAbove (g '' (S Set.Ioi c))) :
            theorem proposition_3_6_2 {S : Set } {c : } {f g : } (hf : MonotoneOn f S) (hg : AntitoneOn g S) :
            (c closure (S Set.Iio c)(BddAbove (f '' (S Set.Iio c))Filter.Tendsto f (nhdsWithin c (S Set.Iio c)) (nhds (sSup (f '' (S Set.Iio c))))) (¬BddAbove (f '' (S Set.Iio c))Filter.Tendsto f (nhdsWithin c (S Set.Iio c)) Filter.atTop) (BddBelow (g '' (S Set.Iio c))Filter.Tendsto g (nhdsWithin c (S Set.Iio c)) (nhds (sInf (g '' (S Set.Iio c))))) (¬BddBelow (g '' (S Set.Iio c))Filter.Tendsto g (nhdsWithin c (S Set.Iio c)) Filter.atBot)) (c closure (S Set.Ioi c)(BddBelow (f '' (S Set.Ioi c))Filter.Tendsto f (nhdsWithin c (S Set.Ioi c)) (nhds (sInf (f '' (S Set.Ioi c))))) (¬BddBelow (f '' (S Set.Ioi c))Filter.Tendsto f (nhdsWithin c (S Set.Ioi c)) Filter.atBot) (BddAbove (g '' (S Set.Ioi c))Filter.Tendsto g (nhdsWithin c (S Set.Ioi c)) (nhds (sSup (g '' (S Set.Ioi c))))) (¬BddAbove (g '' (S Set.Ioi c))Filter.Tendsto g (nhdsWithin c (S Set.Ioi c)) Filter.atTop)) ((Filter.atTopFilter.principal S).NeBot(BddAbove (f '' S)Filter.Tendsto f (Filter.atTopFilter.principal S) (nhds (sSup (f '' S)))) (¬BddAbove (f '' S)Filter.Tendsto f (Filter.atTopFilter.principal S) Filter.atTop) (BddBelow (g '' S)Filter.Tendsto g (Filter.atTopFilter.principal S) (nhds (sInf (g '' S)))) (¬BddBelow (g '' S)Filter.Tendsto g (Filter.atTopFilter.principal S) Filter.atBot)) ((Filter.atBotFilter.principal S).NeBot(BddBelow (f '' S)Filter.Tendsto f (Filter.atBotFilter.principal S) (nhds (sInf (f '' S)))) (¬BddBelow (f '' S)Filter.Tendsto f (Filter.atBotFilter.principal S) Filter.atBot) (BddAbove (g '' S)Filter.Tendsto g (Filter.atBotFilter.principal S) (nhds (sSup (g '' S)))) (¬BddAbove (g '' S)Filter.Tendsto g (Filter.atBotFilter.principal S) Filter.atTop))

            Proposition 3.6.2: Let S ⊆ ℝ, c ∈ ℝ, f : ℝ → ℝ be increasing on S, and g : ℝ → ℝ be decreasing on S. If c is a cluster point of S ∩ (-∞, c), then lim_{x → c^-} f x = sup {f x | x ∈ S, x < c} and lim_{x → c^-} g x = inf {g x | x ∈ S, x < c}. If c is a cluster point of S ∩ (c, ∞), then lim_{x → c^+} f x = inf {f x | x ∈ S, x > c} and lim_{x → c^+} g x = sup {g x | x ∈ S, x > c}. If is a cluster point of S, then lim_{x → ∞} f x = sup {f x | x ∈ S} and lim_{x → ∞} g x = inf {g x | x ∈ S}. If -∞ is a cluster point of S, then lim_{x → -∞} f x = inf {f x | x ∈ S} and lim_{x → -∞} g x = sup {g x | x ∈ S}.

            theorem closure_left_slice_of_ordConnected {I : Set } (hI : I.OrdConnected) {c : I} (hleft : xI, x < c) :
            c closure (I Set.Iio c)

            If an interval I contains a point strictly to the left of c, then c is a closure point of I ∩ (-∞, c).

            theorem closure_right_slice_of_ordConnected {I : Set } (hI : I.OrdConnected) {c : I} (hright : xI, c < x) :
            c closure (I Set.Ioi c)

            If an interval I contains a point strictly to the right of c, then c is a closure point of I ∩ (c, ∞).

            theorem monotone_range_interval_iff_continuous {I : Set } (hI : I.OrdConnected) {f : I} (hf : Monotone f) (hconst : ∃ (x : I) (y : I), f x f y) :

            Corollary 3.6.3: If I ⊆ ℝ is an interval and f : I → ℝ is monotone and not constant, then the image f(I) is an interval if and only if f is continuous.

            theorem monotone_discontinuities_countable {I : Set } (hI : I.OrdConnected) {f : I} (hf : Monotone f) :

            Corollary 3.6.4: Let I ⊆ ℝ be an interval and f : I → ℝ be monotone. Then f has at most countably many discontinuities.

            theorem example_3_6_5 :
            ∃ (f : ), StrictMonoOn f (Set.Icc 0 1) BddBelow (f '' Set.Icc 0 1) BddAbove (f '' Set.Icc 0 1) (∀ (k : ), ¬ContinuousAt f (1 - 1 / k.succ)) {x : | x Set.Icc 0 1 ¬ContinuousAt f x}.Countable

            Example 3.6.5: There exists a strictly increasing function f : [0, 1] → ℝ that is bounded and has a discontinuity at each point 1 - 1/k for k ∈ ℕ. In particular, it is monotone on a compact interval with countably many discontinuities.

            theorem proposition_3_6_6 {I : Set } (hI : I.OrdConnected) {f : I} (hf : StrictMono f) (hTop : OrderTopology (Set.range f)) :

            Proposition 3.6.6: If I ⊆ ℝ is an interval and f : I → ℝ is strictly monotone, then the inverse f⁻¹ : f(I) → I is continuous.

            theorem example_3_6_7 :
            have f := fun (x : ) => if x < 0 then x else x + 1; have S := {y : | y < 0 1 y}; have g := fun (y : S) => if y < 0 then y else y - 1; ¬ContinuousAt f 0 f '' Set.univ = S Continuous g

            Example 3.6.7: The piecewise function f : ℝ → ℝ given by f x = x for x < 0 and f x = x + 1 for x ≥ 0 is not continuous at 0, its image of is (-∞, 0) ∪ [1, ∞), and the inverse function f⁻¹ : (-∞, 0) ∪ [1, ∞) → ℝ defined by y if y < 0 and y - 1 if y ≥ 1 is continuous.