MonotoneOn.mapsTo_Icc
theorem MonotoneOn.mapsTo_Icc :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
MonotoneOn f (Set.Icc a b) → Set.MapsTo f (Set.Icc a b) (Set.Icc (f a) (f b))
This theorem states that for any function `f` from a type `α` to a type `β`, where `α` and `β` have a predefined order, and for any `a` and `b` of type `α`, if the function `f` is monotone on the closed interval `[a, b]`, then the image of the interval `[a, b]` under the function `f` is contained within the closed interval `[f(a), f(b)]`. In other words, a monotone function maps any closed interval, in its original space, to a closed interval in its target space.
More concisely: If `f` is a monotone function from a type `α` to a type `β` with predefined order, then `[f(a), f(b)]` contains the image `{f(x) | x ∈ [a, b]}` of the closed interval `[a, b]` under `f`.
|
AntitoneOn.mapsTo_Icc
theorem AntitoneOn.mapsTo_Icc :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
AntitoneOn f (Set.Icc a b) → Set.MapsTo f (Set.Icc a b) (Set.Icc (f b) (f a))
The theorem `AntitoneOn.mapsTo_Icc` states that for all types `α` and `β`, a function `f` from `α` to `β`, and any elements `a` and `b` of type `α`, if that function `f` is antitone on the interval `Set.Icc a b` (i.e., for all `a, b` in this interval, `a ≤ b` implies `f b ≤ f a`), then the function `f` maps the interval `Set.Icc a b` to the interval `Set.Icc (f b) (f a)`. In other words, all the values `f x` for `x` in the interval from `a` to `b` fall within the interval from `f b` to `f a`. This theorem is about the behavior of an antitone function on a closed interval in a preordered set.
More concisely: If a function between two preordered types is antitone on an interval, then it maps that interval to a reversed interval.
|