IsLocalExtrOn.elim
theorem IsLocalExtrOn.elim :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α}
{p : Prop}, IsLocalExtrOn f s a → (IsLocalMinOn f s a → p) → (IsLocalMaxOn f s a → p) → p
The theorem `IsLocalExtrOn.elim` states that for any topological space `α`, any preorder `β`, any function `f` from `α` to `β`, any set `s` of `α`, and any element `a` of `α`, if `f` has a local extremum at `a` on `s` (meaning it is either a local minimum or a local maximum at `a` on `s`), then any property `p` that holds when `f` has a local minimum at `a` on `s` and also holds when `f` has a local maximum at `a` on `s`, must hold. This uses the principle of disjunction elimination: since `f` having a local extremum at `a` on `s` means `f` is either a local minimum at `a` on `s` or a local maximum at `a` on `s`, if `p` holds in both cases, `p` must hold.
More concisely: If a function `f` has a local extremum at `a` in a set `s` of a topological space `α` with respect to a preorder `β`, then any property `p` that holds for local minima and local maxima of `f` at `a` in `s` also holds.
|
IsLocalExtr.elim
theorem IsLocalExtr.elim :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {a : α} {p : Prop},
IsLocalExtr f a → (IsLocalMin f a → p) → (IsLocalMax f a → p) → p
The theorem `IsLocalExtr.elim` states that for any type `α` equipped with a topology and any type `β` equipped with a preorder, given a function `f : α → β` and an element `a : α`, if `a` is a local extremum of `f` (either a local minimum or a local maximum), then any proposition `p` that holds when `a` is a local minimum of `f` and when `a` is a local maximum of `f` also holds. In other words, this theorem allows us to analyze all local extrema (minima and maxima) of `f` in a unified way.
More concisely: If a function `f` from a topological space `α` to a preordered type `β` has `a` as a local extremum, then any proposition `p` invariant under interchanging local minima and maxima holds at `a`.
|