MonotoneOn.exists_monotone_extension
theorem MonotoneOn.exists_monotone_extension :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β] {f : α → β}
{s : Set α}, MonotoneOn f s → BddBelow (f '' s) → BddAbove (f '' s) → ∃ g, Monotone g ∧ Set.EqOn f g s
The theorem states that if a function is monotone on a set `s` and this function's image (the values it produces) is both lower and upper bounded, then there exists an extension of this function that is monotone over the entire space and is equal to the original function on the set `s`. This is true for all functions from a space `α` to a space `β`, where `α` is a linear ordered set and `β` is a conditionally complete linear ordered set.
More concisely: If a monotone function with a lower and upper bound on a linearly ordered set `α` has a value set in a conditionally complete linearly ordered set `β`, then it has a monotone extension to all of `α` that agrees with the original function on `s`.
|
AntitoneOn.exists_antitone_extension
theorem AntitoneOn.exists_antitone_extension :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β] {f : α → β}
{s : Set α}, AntitoneOn f s → BddBelow (f '' s) → BddAbove (f '' s) → ∃ g, Antitone g ∧ Set.EqOn f g s
The theorem states that given a function `f` from an ordered type `α` to an ordered type `β`, and a set `s` of type `α`, if `f` is antitone on `s` (meaning that for all `a, b` in `s`, if `a` is less than or equal to `b`, then `f(b)` is less than or equal to `f(a)`), and the image of `s` under `f` is both bounded below and above, then there exists an extension of `f` to the whole space, denoted by `g`, that is antitone (meaning that for all `a, b` in the domain of `g`, if `a` is less than or equal to `b`, then `g(b)` is less than or equal to `g(a)`) and `g` is equal to `f` on `s`.
More concisely: Given an antitone function `f` from an ordered `α` to an ordered `β` with domain `s` that maps `s` to a bounded subset of `β`, there exists an extension `g` of `f` to all of `α` that is also antitone and equal to `f` on `s`.
|