IsMinFilter.comp_antitone
theorem IsMinFilter.comp_antitone :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {l : Filter α}
{a : α}, IsMinFilter f l a → ∀ {g : β → γ}, Antitone g → IsMaxFilter (g ∘ f) l a
The theorem `IsMinFilter.comp_antitone` states that for all types `α`, `β`, and `γ`, if `β` and `γ` are preordered, and given a function `f` from `α` to `β`, a filter `l` on `α`, and an element `a` of `α` such that `f` has a local minimum at `a` with respect to `l` (i.e., `f a` is less than or equal to `f x` for all `x` near `a`), then for any function `g` from `β` to `γ` that is antitone (i.e., if `b` is greater than or equal to `a` then `g(b)` is less than or equal to `g(a)`), the composed function `g ∘ f` has a local maximum at `a` with respect to `l`. In other words, if `f` is minimized at some point under some conditions, the composition of `f` with an antitone function will be maximized at that point under the same conditions.
More concisely: If `f: α → β` has a local minimum at `a` with respect to filter `l` on `α`, and `g: β → γ` is antitone, then `g ∘ f` has a local maximum at `a` with respect to `l`.
|
IsMaxFilter.undual
theorem IsMaxFilter.undual :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter (⇑OrderDual.toDual ∘ f) l a → IsMinFilter f l a
The theorem `IsMaxFilter.undual` states that for any given types α and β, where β has a preorder structure, and any function `f` from α to β, filter `l` on α, and element `a` of α, if `f` composed with the function `OrderDual.toDual` (which is effectively an identity function on the dual ordering of the given type) is a maximal filter at `a`, then `f` is a minimal filter at `a`. In other words, if for all points `x` in some neighborhood of `a` (defined by the filter `l`), the function values `f(x)` are less than or equal to `f(a)` when considered under the dual order, then for that same set of points `x`, `f(a)` is less than or equal to `f(x)` under the original order.
More concisely: If a filter `l` on type `α` and an element `a` in `α` satisfy that the composite function `f ∘ OrderDual.toDual` is a maximal filter at `a` for a function `f: α → β` with `β` having a preorder structure, then `f` is a minimal filter at `a`.
|
IsMaxFilter.neg
theorem IsMaxFilter.neg :
∀ {α : Type u} {β : Type v} [inst : OrderedAddCommGroup β] {f : α → β} {a : α} {l : Filter α},
IsMaxFilter f l a → IsMinFilter (fun x => -f x) l a
The theorem `IsMaxFilter.neg` states that for any type `α`, any ordered additive commutative group `β`, any function `f` from `α` to `β`, any filter `l` on `α`, and any element `a` of `α`, if `f` attains its maximum value at `a` within some neighborhood defined by the filter `l` (in other words, if `f x ≤ f a` for all `x` in the `l`-neighborhood of `a`), then the function `-f` (which negates the output of `f`) attains its minimum value at the same point `a` within the same neighborhood (that is, `(-f) a ≤ (-f) x` for all `x` in the `l`-neighborhood of `a`). This means that the negation of a function that has a maximum at a certain point will have a minimum at that same point.
More concisely: If a function f from a type α to an ordered additive commutative group β attains a maximum at a point a within a filter l on α, then the negation of f attains a minimum at a.
|
IsMaxFilter.inf
theorem IsMaxFilter.inf :
∀ {α : Type u} {β : Type v} [inst : SemilatticeInf β] {f g : α → β} {a : α} {l : Filter α},
IsMaxFilter f l a → IsMaxFilter g l a → IsMaxFilter (fun x => f x ⊓ g x) l a
The theorem `IsMaxFilter.inf` states that for any type `α`, `β` where `β` forms a semilattice under the infimum operation, and for any two functions `f` and `g` from `α` to `β`, any point `a` in `α`, and any filter `l` on `α`, if `a` is a maximum point for both `f` and `g` with respect to `l`, then `a` is also a maximum point for the function defined by the infimum of `f` and `g` at each point, with respect to the same filter `l`. In other words, if `f(x) ≤ f(a)` and `g(x) ≤ g(a)` for all `x` in some `l`-neighborhood of `a`, then `(f(x) ⊓ g(x)) ≤ (f(a) ⊓ g(a))` for all such `x`.
More concisely: Given types `α` and `β` with `β` being a semilattice under infimum, functions `f` and `g` from `α` to `β`, a filter `l` on `α`, and a point `a` in `α` maximizing both `f` and `g` with respect to `l`, then `a` maximizes the infimum of `f` and `g` with respect to the same filter `l`. In other words, if `f(x) ≤ f(a)` and `g(x) ≤ g(a)` for all `x` in some `l`-neighborhood of `a`, then `(f ⊓ g)(x) ≤ (f ⊓ g)(a)` for all such `x`.
|
IsMinFilter.dual
theorem IsMinFilter.dual :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter f l a → IsMaxFilter (⇑OrderDual.toDual ∘ f) l a
The theorem `IsMinFilter.dual` states that for any types `α` and `β` with a preorder on `β`, and for any function `f` from `α` to `β`, any filter `l` on `α` and any element `a` of `α`, if `a` is a minimum of the function `f` on the set of elements in the filter neighborhood `l`, then `a` is a maximum of the function `f` composed with the identity function to the `OrderDual` of `β` on the same set. In other words, it states that the concept of minimality for a function in a certain set is equivalent to the concept of maximality for the same function on the dual order of the co-domain, applied to the same set.
More concisely: For any function between preordered types and a filter on the domain, an element is a minimum of the function on the filter neighborhood if and only if it is a maximum of the function composed with the order dual on the same neighborhood.
|
IsMinFilter.min
theorem IsMinFilter.min :
∀ {α : Type u} {β : Type v} [inst : LinearOrder β] {f g : α → β} {a : α} {l : Filter α},
IsMinFilter f l a → IsMinFilter g l a → IsMinFilter (fun x => min (f x) (g x)) l a
The theorem `IsMinFilter.min` states that for any given types `α` and `β`, where `β` is a linear order, any two functions `f` and `g` from `α` to `β`, any point `a` of type `α`, and any filter `l` on `α`, if `a` is a minimum of both `f` and `g` under the filter `l`, then `a` is also a minimum of the function that takes `x` to the minimum of `f(x)` and `g(x)` under the same filter `l`. In mathematical terms, if `f(a) ≤ f(x)` for all `x` in a certain `l`-neighborhood of `a`, and `g(a) ≤ g(x)` for all `x` in the same `l`-neighborhood, then the minimum of `f(a)` and `g(a)` is less than or equal to the minimum of `f(x)` and `g(x)` for all `x` in that `l`-neighborhood.
More concisely: If functions `f` and `g` from type `α` to a linear order `β`, and point `a` in `α` is a minimum of both `f` and `g` under filter `l`, then the point `a` is also a minimum of the function `x ↦ min(f(x), g(x))` under the same filter `l`.
|
isMinFilter_const
theorem isMinFilter_const :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {a : α} {b : β}, IsMinFilter (fun x => b) l a := by
sorry
The theorem `isMinFilter_const` states that for all types `α` and `β`, where `β` has a preorder (meaning that it has a binary relation satisfying reflexivity and transitivity), for all filters `l` on `α`, for all elements `a` of `α`, and for all elements `b` of `β`, the function that sends every element to `b` (a constant function) is a minimum filter at `a` with respect to `l`. In other words, the value of `b` is less than or equal to the value of the function at any other point in the `l`-neighborhood of `a`. This is always the case for a constant function, since all function values are the same, namely `b`.
More concisely: For all types `α` and preordered `β`, given a filter `l` on `α`, a constant function `f : α → β` with value `b` at every point, and any `a` in `α`, `b` is an `l`-minimum at `a`.
|
IsMaxFilter.comp_antitone
theorem IsMaxFilter.comp_antitone :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {l : Filter α}
{a : α}, IsMaxFilter f l a → ∀ {g : β → γ}, Antitone g → IsMinFilter (g ∘ f) l a
The theorem `IsMaxFilter.comp_antitone` states that for all types `α`, `β`, and `γ` with `β` and `γ` equipped with a preorder, and for any filter `l` over `α`, any function `f : α → β`, and any element `a` of `α`, if `f` achieves its maximum at `a` with respect to the filter `l`, then for any antitone function `g : β → γ`, the composed function `g ∘ f` achieves its minimum at `a` with respect to the filter `l`. In other words, if `f` is maximized at `a` and `g` decreases when its input increases, then `g(f(x))` is minimized at `a`.
More concisely: For all types `α`, `β`, and `γ` with `β` and `γ` preordered, if a filter `l` over `α`, function `f : α → β`, and element `a` of `α` satisfy `f(a) = max filter l a`, then `g ∘ f(a) = min filter l (g ∘ f) a` for any antitone function `g : β → γ`.
|
IsMinFilter.bicomp_mono
theorem IsMinFilter.bicomp_mono :
∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β}
{l : Filter α} {a : α} [inst_2 : Preorder δ] {op : β → γ → δ},
((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op op →
IsMinFilter f l a → ∀ {g : α → γ}, IsMinFilter g l a → IsMinFilter (fun x => op (f x) (g x)) l a
This theorem states that for any types `α`, `β`, `γ`, and `δ`, given a preorder on `β`, `γ`, and `δ`, a function `f` from `α` to `β`, a filter `l` on `α`, an element `a` of `α`, and an operation `op` from `β` and `γ` to `δ` that preserves the preorder (meaning that if `x ≤ y`, then `op x z ≤ op y z` and `op z x ≤ op z y` for any `z`), if `f` and `g` (a function from `α` to `γ`) are both minimum filters at `a` with respect to `l`, then the function which applies `op` to `f x` and `g x` for each `x` in `α` is also a minimum filter at `a` with respect to `l`.
In other words, if `f` and `g` are both functions from `α` to `β` and `γ` respectively such that `f a` and `g a` are less than or equal to all other values of `f` and `g` in some neighborhood of `a`, then, for an operation `op` that preserves the preorder, the value of `op (f a) (g a)` is less than or equal to the values of `op (f x) (g x)` for all `x` in the same neighborhood of `a`. This theorem generalizes the concept of a minimum in a mathematical setting.
More concisely: Given functions `f: α -> β`, `g: α -> γ`, and an operation `op: β x γ -> δ` preserving the preorder on `β`, `γ`, and `δ`, if `f` and `g` are minimum filters at `a` in `α` with respect to a filter `l`, then the function `x => op (f x) (g x)` is also a minimum filter at `a` with respect to `l`.
|
IsMinOn.dual
theorem IsMinOn.dual :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMinOn f s a → IsMaxOn (⇑OrderDual.toDual ∘ f) s a
The theorem `IsMinOn.dual` states that for any types `α` and `β`, with a preorder defined on `β`, and any function `f` from `α` to `β`, any set `s` of type `α`, and any element `a` of type `α`, if `a` minimizes the function `f` over the set `s` (i.e., `f(a)` is less than or equal to `f(x)` for all `x` in `s`), then `a` also maximizes the function `f` under the dual order over the set `s` (i.e., `f(a)` is greater than or equal to `f(x)` for all `x` in `s` under the dual order). The dual order is the reverse of the original preorder on `β`. This essentially means that the minimum value in the original order becomes the maximum value in the dual order.
More concisely: For any function `f` from a type `α` to a type `β` with a preorder, if an element `a` of type `α` minimizes `f` over a set `s` of type `α`, then it maximizes `f` under the dual preorder over `s`.
|
IsMinFilter.inf
theorem IsMinFilter.inf :
∀ {α : Type u} {β : Type v} [inst : SemilatticeInf β] {f g : α → β} {a : α} {l : Filter α},
IsMinFilter f l a → IsMinFilter g l a → IsMinFilter (fun x => f x ⊓ g x) l a
The theorem `IsMinFilter.inf` states that for any two functions `f` and `g` from a type `α` to a type `β`, and for a specific value `a` of type `α` and a filter `l` on `α`, if `a` is a minimum point for both `f` and `g` with respect to the filter `l` (in other words, if for all `x` in some `l`-neighborhood of `a`, the value of `f` and `g` at `a` is less than or equal to the value of `f` and `g` at `x`), then `a` is also a minimum point for the function that takes `x` to the infimum of `f(x)` and `g(x)` with respect to the same filter `l`. The type `β` is assumed to be a semilattice with respect to the infimum operation.
More concisely: If `a` is a minimum point for both `f` and `g` with respect to filter `l` on type `α`, then `a` is also a minimum point for the function `x => inf (f x) (g x)` with respect to the same filter `l`, where `inf` denotes the infimum operation in semilattice `β`.
|
IsMinFilter.neg
theorem IsMinFilter.neg :
∀ {α : Type u} {β : Type v} [inst : OrderedAddCommGroup β] {f : α → β} {a : α} {l : Filter α},
IsMinFilter f l a → IsMaxFilter (fun x => -f x) l a
The theorem `IsMinFilter.neg` states that for any type `α`, any ordered additive commutative group `β`, any function `f` from `α` to `β`, any element `a` of type `α`, and any filter `l` on `α`, if `f` reaches its minimum value at `a` within the neighborhood of `a` defined by the filter `l` (i.e., `f(a)` is less than or equal to `f(x)` for all `x` in that neighborhood), then the negative of `f`, `-f`, reaches its maximum value at the same point `a` within the same neighborhood (i.e., `-f(a)` is greater than or equal to `-f(x)` for all `x` in that neighborhood). This theorem essentially states that the point of minimum value for a function in a certain neighborhood becomes the point of maximum value for the negative of that function in the same neighborhood.
More concisely: For any function `f` from a type `α` to an ordered additive commutative group `β`, if `a` is the point where `f` achieves its minimum value within the neighborhood defined by filter `l` on `α`, then `-a` is the point where `-f` achieves its maximum value within the same neighborhood.
|
isMaxFilter_const
theorem isMaxFilter_const :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {a : α} {b : β}, IsMaxFilter (fun x => b) l a := by
sorry
The theorem `isMaxFilter_const` states that for any types `α` and `β`, any preorder on `β`, any filter `l` on `α`, any element `a` of `α`, and any element `b` of `β`, the constant function that maps every element of `α` to `b` is a maximum filter at `a` with respect to `l`. This essentially means that `b` is greater than or equal to the value of this function at any other point in some neighborhood of `a` determined by the filter `l`.
More concisely: For any filter $l$ on type $\alpha$, any element $a$ in $\alpha$, and any constant function $f : \alpha \rightarrow \beta$ with $f(a) = b$, $b$ is an upper bound of $l$ at $a$, i.e., for all $x \in \mathop{\mathrm{st}}{} l(a)$, $f(x) \geq b$.
|
IsExtrFilter.comp_antitone
theorem IsExtrFilter.comp_antitone :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {l : Filter α}
{a : α}, IsExtrFilter f l a → ∀ {g : β → γ}, Antitone g → IsExtrFilter (g ∘ f) l a
The theorem `IsExtrFilter.comp_antitone` states that for all types `α`, `β`, and `γ`, given a preorder on `β` and `γ`, for any function `f` from `α` to `β`, any filter `l` on `α`, and any member `a` of `α`, if `f` is an extremal filter at `a` and `g` is an antitone function from `β` to `γ`, then the composition `g ∘ f` is also an extremal filter at `a`. In other words, the composition of an extremal function and an antitone function preserves the extremality at any given point under a specified filter.
More concisely: If `f: α → β` is an extremal filter function at `a ∈ α`, `g: β → γ` is an antitone function, and `l` is a filter on `α`, then `g ∘ f` is an extremal filter at `a` with respect to `l`.
|
IsMinFilter.isExtr
theorem IsMinFilter.isExtr :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter f l a → IsExtrFilter f l a
The theorem `IsMinFilter.isExtr` states that for any types `α` and `β` with a preorder on `β`, and given a function `f` from `α` to `β`, a filter `l` on `α`, and an element `a` of `α`, if `a` is a minimum of the function `f` in some neighborhood defined by the filter `l` (meaning `f(a)` is less than or equal to `f(x)` for all `x` in that neighborhood), then `a` is also an extremum in that neighborhood (meaning `a` is either a minimum or a maximum of `f` in that neighborhood).
More concisely: If `a` is a minimum of the function `f` in the neighborhood defined by filter `l` on type `α`, then `a` is an extremum (minimum or maximum) of `f` in that neighborhood.
|
IsMaxFilter.min
theorem IsMaxFilter.min :
∀ {α : Type u} {β : Type v} [inst : LinearOrder β] {f g : α → β} {a : α} {l : Filter α},
IsMaxFilter f l a → IsMaxFilter g l a → IsMaxFilter (fun x => min (f x) (g x)) l a
The theorem `IsMaxFilter.min` states that for all types `α` and `β`, where `β` has a linear order, for all functions `f` and `g` from `α` to `β`, for all elements `a` of type `α`, and for all filters `l` on `α`, if `f` has a maximum at `a` with respect to the filter `l` and `g` also has a maximum at `a` with respect to the same filter `l`, then the function that assigns to each element `x` the minimum of `f(x)` and `g(x)` also has a maximum at `a` with respect to the filter `l`. In other words, if `f` and `g` both have their maximum values (in the order of `β`) at `a` within a neighborhood defined by `l`, then the minimum of `f` and `g` at each point also achieves its maximum value at `a` within the same neighborhood.
More concisely: If functions `f` and `g` have equal maximum values at `a` with respect to filter `l` on type `α`, then the function `x ↔> min (f x) (g x)` has a maximum at `a` with respect to filter `l` on type `α`, where `min` is the pointwise minimum and `↔>` is the reverse arrow denoting maximum.
|
IsMinFilter.max
theorem IsMinFilter.max :
∀ {α : Type u} {β : Type v} [inst : LinearOrder β] {f g : α → β} {a : α} {l : Filter α},
IsMinFilter f l a → IsMinFilter g l a → IsMinFilter (fun x => max (f x) (g x)) l a
The theorem `IsMinFilter.max` states that for any types `α` and `β` with `β` having a `LinearOrder` structure, and any functions `f` and `g` from `α` to `β`, if `f` and `g` are both minimizing functions with respect to some filter `l` at a point `a` (i.e., their values at `a` are less than or equal to their values for all points in some `l`-neighborhood of `a`), then the function that takes the maximum of `f` and `g` at each point is also a minimizing function with respect to the same filter `l` at the same point `a`. In other words, if `f(a) ≤ f(x)` for all `x` near `a` and `g(a) ≤ g(x)` for all `x` near `a`, then `max(f(a), g(a)) ≤ max(f(x), g(x))` for all `x` near `a`.
More concisely: If functions `f` and `g` are both minimizers with respect to filter `l` at point `a`, then the pointwise maximum `\max(f, g)` is also a minimizer with respect to filter `l` at point `a`.
|
IsMaxOn.dual
theorem IsMaxOn.dual :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMaxOn f s a → IsMinOn (⇑OrderDual.toDual ∘ f) s a
The theorem `IsMaxOn.dual` states that for any set `s` and any element `a` from a type `α`, if `a` is a maximizing element for a function `f` on the set `s`, then it is also a minimizing element for the function `f` composed with the identity function on `s` in the dual order. This means that the maximum value of `f` in the original order becomes the minimum value in the reversed (dual) order. The types `α` and `β` are any types, with a preorder defined on `β`.
More concisely: If `a` is a maximum of `f` over `s`, then `a` is a minimum of `f ∘ id` in the dual order on `β`.
|
IsExtrOn.dual
theorem IsExtrOn.dual :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsExtrOn f s a → IsExtrOn (⇑OrderDual.toDual ∘ f) s a
The theorem `IsExtrOn.dual` says that for any types `α` and `β`, with `β` being a preorder, any function `f` from `α` to `β`, any set `s` of type `α`, and any element `a` of type `α`, if `f` has an extremal value (either a minimum or a maximum) at `a` on the set `s`, then the function obtained by composing `f` with the identity function to the "dual" order also has an extremal value at `a` on the set `s`. In other words, applying the order-duality transformation preserves the locations of extremal values of a function.
More concisely: If a function from type `α` to a preorder `β` attains an extremum at an element `a` in a set `s` of type `α`, then the composition of `f` with the identity function to the dual order also attains an extremum at `a` in `s`.
|
IsMaxFilter.congr
theorem IsMaxFilter.congr :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : α → β} {a : α} {l : Filter α},
IsMaxFilter f l a → l.EventuallyEq f g → f a = g a → IsMaxFilter g l a
The theorem `IsMaxFilter.congr` states that for any two functions `f` and `g` from a type `α` to an ordered type `β`, if `f` has a property that it reaches its maximum (`IsMaxFilter`) at a point `a` according to some `l`-neighborhood, and `f` equals `g` almost everywhere in this `l`-neighborhood, and moreover `f(a) = g(a)`, then `g` also has the `IsMaxFilter` property at `a` with respect to the same `l`-neighborhood. In other words, if `f` and `g` are essentially the same in the `l`-neighborhood of `a` and `f` attains its maximum at `a`, then `g` also attains its maximum at `a`.
More concisely: If functions `f` and `g` from type `α` to an ordered type `β` agree and have maximum value at point `a` within an `l`-neighborhood, then `g` also has maximum value at `a` within that same `l`-neighborhood.
|
IsMaxFilter.bicomp_mono
theorem IsMaxFilter.bicomp_mono :
∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β}
{l : Filter α} {a : α} [inst_2 : Preorder δ] {op : β → γ → δ},
((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op op →
IsMaxFilter f l a → ∀ {g : α → γ}, IsMaxFilter g l a → IsMaxFilter (fun x => op (f x) (g x)) l a
The theorem `IsMaxFilter.bicomp_mono` states that for all types `α`, `β`, `γ`, and `δ` that are preordered, given a function `f` from `α` to `β`, a filter `l` on `α`, and an element `a` of `α`, if there exists an operator `op` from `β` and `γ` to `δ` such that this operator is monotonic with respect to both its arguments, and if `f` and another function `g` from `α` to `γ` are both maximum filters at `a` with respect to the filter `l`, then the function that maps `x` to `op (f x) (g x)` is also a maximum filter at `a` with respect to the filter `l`. In simpler terms, under these conditions, taking the `op` of the values of `f` and `g` at any point in a neighborhood of `a` will always be less than or equal to the `op` of the values of `f` and `g` at `a` itself.
More concisely: If `f` and `g` are maximum filters at `a` with respect to a filter `l` on types `α`, `β`, `γ`, and `δ` preordered by `≤`, and there exists a monotonic operator `op` from `β` and `γ` to `δ`, then the function `x ↦ op (f x) (g x)` is also a maximum filter at `a` with respect to `l`.
|
IsExtrFilter.dual
theorem IsExtrFilter.dual :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsExtrFilter f l a → IsExtrFilter (⇑OrderDual.toDual ∘ f) l a
This theorem, referred to as an alias of the reverse direction of `isExtrFilter_dual_iff`, states that for any given type `α`, type `β` with a preorder, a function `f` from `α` to `β`, a filter `l` on `α`, and an element `a` of `α`, if `a` is an extremum of the function `f` with respect to the filter `l` (i.e., `a` is either a minimum or a maximum of `f` in `l`), then `a` is also an extremum of the function obtained by composing `f` with the identity function on the order dual of `β`. This means that the property of being an extremum for a function is preserved under the order-dual operation.
More concisely: For any type `α`, type `β` with a preorder, a function `f` from `α` to `β`, a filter `l` on `α`, and an element `a` of `α`, if `a` is an extremum of `f` with respect to `l`, then `a` is also an extremum of `f ∘ id^dual`, where `id^dual` is the identity function on the order dual of `β`.
|
IsMaxOn.undual
theorem IsMaxOn.undual :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMaxOn (⇑OrderDual.toDual ∘ f) s a → IsMinOn f s a
The theorem `IsMaxOn.undual` states that, for any given types `α` and `β` under a preorder relationship, given a function `f` from `α` to `β`, a set `s` of type `α`, and an element `a` of type `α`, if `a` is the maximum value in the set `s` when evaluated via the function `f` under the order dual, then `a` is the minimum value in the set `s` when evaluated via the function `f`. In simpler terms, this theorem relates the concept of maximality under a certain function in a dual order to the concept of minimality under the same function in the original order.
More concisely: If `a` is the maximum value of `s` under the function `f` in the order dual, then `a` is the minimum value of `s` under `f` in the original order.
|
IsExtrOn.undual
theorem IsExtrOn.undual :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsExtrOn (⇑OrderDual.toDual ∘ f) s a → IsExtrOn f s a
The theorem `IsExtrOn.undual` states that for any given type `α` and a `Preorder` on type `β`, if a function `f` from `α` to `β` is extreme (i.e., either minimum or maximum) on a set `s` of `α` at a point `a` in the 'dual' sense (i.e., considering the opposite order), then it is also extreme on the set `s` in the original order. In other words, taking the dual of the order doesn't affect where the function reaches its extreme values.
More concisely: If a function from a type to a preordered type attains an extreme value in the dual order at a point in the domain over a set, then it also attains that extreme value in the original order over the same set.
|
IsMaxFilter.isExtr
theorem IsMaxFilter.isExtr :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter f l a → IsExtrFilter f l a
The theorem `IsMaxFilter.isExtr` states that for all types `α` and `β`, where `β` has a preorder structure, and for all functions `f` from `α` to `β`, filters `l` on `α`, and elements `a` of `α`, if `a` is a maximum point for `f` within some neighborhood determined by `l` (i.e., `f(x) ≤ f(a)` for all `x` in this neighborhood), then `a` is an extremal point for `f` with respect to this filter `l`. In other words, if `a` is a local maximum for `f`, it is also a local extremum (either a local maximum or minimum).
More concisely: For any type `α` with preorder `β`, given a function `f` from `α` to `β`, an element `a` in `α`, and a filter `l` on `α`, if `a` is a maximum point of `f` within `l`'s neighborhood, then `a` is an extremal point for `f` with respect to `l`.
|
IsMinFilter.congr
theorem IsMinFilter.congr :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : α → β} {a : α} {l : Filter α},
IsMinFilter f l a → l.EventuallyEq f g → f a = g a → IsMinFilter g l a
The theorem `IsMinFilter.congr` states that for any two functions `f` and `g` from a type `α` to a type `β` with a preorder, if `f` is a minimal element in some filter `l` around a point `a` (meaning `f a` is less than or equal to `f x` for all `x` in a neighborhood defined by `l`), and if `f` and `g` are eventually equal in the filter `l`, and `f a` equals `g a`, then `g` is also a minimal element in the filter `l` around `a`. This theorem is a congruence property for minimality under a filter.
More concisely: If functions `f` and `g` from type `α` to type `β` with a preorder have equal values at a point `a`, are eventually equal in a filter `l` around `a`, and `f` is minimal in `l` around `a`, then `g` is also minimal in `l` around `a`.
|
IsMaxFilter.max
theorem IsMaxFilter.max :
∀ {α : Type u} {β : Type v} [inst : LinearOrder β] {f g : α → β} {a : α} {l : Filter α},
IsMaxFilter f l a → IsMaxFilter g l a → IsMaxFilter (fun x => max (f x) (g x)) l a
The theorem `IsMaxFilter.max` states that for any two functions `f` and `g` from any type `α` to any type `β`, with `β` possessing a linear order, if `f` and `g` both satisfy the `IsMaxFilter` property at a point `a` with respect to a filter `l`, then the function which to every `x` assigns the maximum of `f(x)` and `g(x)` also satisfies the `IsMaxFilter` property at `a` with respect to `l`. In other words, if `f x ≤ f a` and `g x ≤ g a` for all `x` in some `l`-neighborhood of `a`, then `max (f x) (g x) ≤ max (f a) (g a)` for all `x` in that `l`-neighborhood.
More concisely: If functions `f` and `g` from type `α` to ordered type `β` satisfy `IsMaxFilter` at point `a` with respect to filter `l`, then the function `x => max (f x) (g x)` also satisfies `IsMaxFilter` at `a` with respect to `l`.
|
IsMaxFilter.add
theorem IsMaxFilter.add :
∀ {α : Type u} {β : Type v} [inst : OrderedAddCommMonoid β] {f g : α → β} {a : α} {l : Filter α},
IsMaxFilter f l a → IsMaxFilter g l a → IsMaxFilter (fun x => f x + g x) l a
The theorem `IsMaxFilter.add` states that for any types `α` and `β`, given an ordered commutative monoid on `β`, any two functions `f` and `g` from `α` to `β`, any point `a` of type `α`, and a filter `l` on `α`, if `f x ≤ f a` for all `x` in some `l`-neighborhood of `a` and `g x ≤ g a` for all `x` in the same `l`-neighborhood, then `(f x + g x) ≤ (f a + g a)` for all `x` in that `l`-neighborhood. In other words, if `f` and `g` both reach their maximum values at `a` when restricted to the `l`-neighborhood of `a`, then their sum also attains its maximum at `a`.
More concisely: For any ordered commutative monoids `β`, given functions `f` and `g` from type `α` to `β`, point `a` of type `α`, filter `l` on `α`, if `f(x) ≤ f(a)` and `g(x) ≤ g(a)` hold for all `x` in the `l`-neighborhood of `a`, then `(f(x) + g(x)) ≤ (f(a) + g(a))` for all `x` in that `l`-neighborhood.
|
IsMaxFilter.comp_tendsto
theorem IsMaxFilter.comp_tendsto :
∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {l : Filter α} {g : δ → α} {l' : Filter δ}
{b : δ}, IsMaxFilter f l (g b) → Filter.Tendsto g l' l → IsMaxFilter (f ∘ g) l' b
The theorem `IsMaxFilter.comp_tendsto` states that for any types `α`, `β`, and `δ` with a preorder relation on `β`, given a function `f : α → β`, a filter `l` on `α`, another function `g : δ → α`, another filter `l'` on `δ`, and a point `b : δ`, if `f` attains its maximum at `g(b)` for all elements in the `l`-neighborhood of `g(b)` (i.e., `IsMaxFilter f l (g b)` holds), and `g` is such that for every `l`-neighborhood `a`, the `g`-preimage of `a` is an `l'`-neighborhood (i.e., `Filter.Tendsto g l' l` holds), then `(f ∘ g)` also attains its maximum at `b` for all elements in the `l'`-neighborhood of `b` (i.e., `IsMaxFilter (f ∘ g) l' b` holds). In simpler words, this theorem ensures that the property of attaining maximum value is preserved under the composition of functions when dealing with filters.
More concisely: If a function `f : α → β` attains its maximum at `g(b)` in the `l`-neighborhood of `g(b)` for some filter `l` on `α`, and `g : δ → α` maps `l'`-neighborhoods to `l`-neighborhoods, then `(f ∘ g)` attains its maximum at `b` in the `l'`-neighborhood of `b`.
|
IsMaxFilter.sup
theorem IsMaxFilter.sup :
∀ {α : Type u} {β : Type v} [inst : SemilatticeSup β] {f g : α → β} {a : α} {l : Filter α},
IsMaxFilter f l a → IsMaxFilter g l a → IsMaxFilter (fun x => f x ⊔ g x) l a
The theorem `IsMaxFilter.sup` states that for any types `α` and `β` where `β` is a semilattice, given two functions `f` and `g` from `α` to `β`, an element `a` of type `α`, and a filter `l` on `α`, if `f` and `g` are both maximized at `a` relative to `l`, then the function whose value at any point is the supremum of `f` and `g` at that point is also maximized at `a` relative to `l`. In other words, if `f(x) ≤ f(a)` and `g(x) ≤ g(a)` for all `x` in some `l`-neighborhood of `a`, then `(f(x) ⊔ g(x)) ≤ (f(a) ⊔ g(a))` for all such `x`.
More concisely: If functions `f` and `g` from type `α` to semilattice `β` are maximized at `a` in filter `l` on `α`, then their pointwise supremum is also maximized at `a` in `l`.
|
IsExtrFilter.undual
theorem IsExtrFilter.undual :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsExtrFilter (⇑OrderDual.toDual ∘ f) l a → IsExtrFilter f l a
The theorem `IsExtrFilter.undual` states that for any types `α` and `β` with a preorder on `β`, for any function `f` from `α` to `β`, for any filter `l` on `α`, and any element `a` of type `α`, if the function `f` composed with the identity function to the `OrderDual` of `β` is an extremal (either minimal or maximal) filter at `a` with respect to `l`, then `f` itself is also an extremal filter at `a` with respect to `l`. In other words, applying the `OrderDual` function - which doesn't change the order - to `f` doesn't change its extremal filter property.
More concisely: If a function `f` from type `α` to a preordered type `β` preserves extremal filters of a filter `l` on `α` at an element `a` in `α`, then `f` itself is an extremal filter for `l` at `a`.
|
Filter.EventuallyLE.isMaxFilter
theorem Filter.EventuallyLE.isMaxFilter :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : α → β} {a : α} {l : Filter α},
l.EventuallyLE g f → f a = g a → IsMaxFilter f l a → IsMaxFilter g l a
The theorem `Filter.EventuallyLE.isMaxFilter` states that for any types `α` and `β`, where `β` has a preorder, for any functions `f` and `g` from `α` to `β`, any element `a` of `α`, and any filter `l` on `α`, if `g` is less than or equal to `f` almost everywhere in the filter `l` and `f(a)` equals `g(a)`, then if `f` has a property that its value at `a` is a maximum among all values in a `l`-neighborhood of `a` (i.e., `f` satisfies the `IsMaxFilter` property at `a` with respect to `l`), then `g` also satisfies the `IsMaxFilter` property at `a` with respect to `l`. This theorem essentially says that if one function is less than or equal to another function almost everywhere within a certain context (the filter `l`), and they are equal at a certain point, then if the larger function has a maximum value at that point within the context, so does the smaller function.
More concisely: If `f` satisfies `IsMaxFilter` property at `a` with respect to filter `l` over `α`, and `g` is less than or equal to `f` almost everywhere in `l`, then `g` also satisfies `IsMaxFilter` property at `a` with respect to `l`.
|
IsMaxFilter.filter_mono
theorem IsMaxFilter.filter_mono :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α},
IsMaxFilter f l a → l' ≤ l → IsMaxFilter f l' a
The theorem `IsMaxFilter.filter_mono` states that for any types `α` and `β`, given a preorder (reflexive and transitive binary relation) on `β`, a function `f` from `α` to `β`, two filters `l` and `l'` on `α`, and an element `a` of type `α`, if `f` is maximized at `a` in some `l`-neighborhood (meaning that the value of `f` at any point in this neighborhood is less than or equal to `f(a)`), and if `l'` is a subfilter of `l` (meaning that every set in `l'` is also in `l`), then `f` is also maximized at `a` in every `l'`-neighborhood. In other words, any subfilter of a filter where `f` has a maximum retains this maximum.
More concisely: Given a preorder, a function, two filters, and an element, if the function is maximized at the element in some neighborhood of the larger filter and the smaller filter is a subfilter, then the function is maximized at the element in every neighborhood of the smaller filter.
|
IsExtrFilter.comp_mono
theorem IsExtrFilter.comp_mono :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {l : Filter α}
{a : α}, IsExtrFilter f l a → ∀ {g : β → γ}, Monotone g → IsExtrFilter (g ∘ f) l a
The theorem `IsExtrFilter.comp_mono` states that for any types `α`, `β`, and `γ`, with preorder relations defined on `β` and `γ`, given a function `f` from `α` to `β`, a filter `l` on `α`, and an element `a` of `α` such that `f` is extreme (either a minimum or a maximum) at `a` with respect to the filter `l`, then for any monotone function `g` from `β` to `γ`, the composition of `g` and `f` (denoted as `g ∘ f`) is also extreme at `a` with respect to the filter `l`. In other words, the extrema of a function are preserved under monotone transformations.
More concisely: If `f: α → β` is extreme with respect to filter `l` on `α` at point `a ∈ α`, and `g: β → γ` is a monotone function, then `g ∘ f` is extreme with respect to filter `l` on `α` at point `a`.
|
IsExtrOn.elim
theorem IsExtrOn.elim :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {p : Prop},
IsExtrOn f s a → (IsMinOn f s a → p) → (IsMaxOn f s a → p) → p
This theorem, `IsExtrOn.elim`, states that for any types `α` and `β` with a preorder on `β`, any function `f` from `α` to `β`, any set `s` of `α`, any element `a` of `α`, and any proposition `p`, if `f` has an extreme value at `a` on the set `s` (denoted by `IsExtrOn f s a`), then if `p` follows from `f` having a minimum at `a` on `s` (denoted by `IsMinOn f s a`) and `p` also follows from `f` having a maximum at `a` on `s` (denoted by `IsMaxOn f s a`), then `p` must hold. This theorem essentially allows us to draw conclusions from the fact that a function has an extreme value (either a maximum or minimum) at a certain point over a set.
More concisely: If a function has an extreme value (minimum or maximum) at a point in a set, and this extreme value property implies a given proposition, then the proposition holds.
|
IsMinFilter.sup
theorem IsMinFilter.sup :
∀ {α : Type u} {β : Type v} [inst : SemilatticeSup β] {f g : α → β} {a : α} {l : Filter α},
IsMinFilter f l a → IsMinFilter g l a → IsMinFilter (fun x => f x ⊔ g x) l a
The theorem `IsMinFilter.sup` states that for any types `α` and `β`, where `β` is a semilattice, and any two functions `f` and `g` from `α` to `β`, and any element `a` of type `α` and any filter `l` on `α`, if `a` is a minimal point of both `f` and `g` with respect to `l` (meaning that for all `x` in some `l`-neighborhood of `a`, `f a` and `g a` are less than or equal to `f x` and `g x` respectively), then `a` is also a minimal point of the function that takes `x` to the sup (least upper bound) of `f x` and `g x` with respect to `l`. In other words, if `a` minimizes both `f` and `g` in some neighborhood defined by `l`, it also minimizes the combined function where each value is the maximum of the corresponding values in `f` and `g`.
More concisely: For any functions `f` and `g` from a type `α` to a semilattice `β`, and any filter `l` on `α`, if an element `a` in `α` is minimal with respect to both `f` and `g` in the neighborhood defined by `l`, then it is also minimal with respect to the function that maps `x` to the sup of `f x` and `g x`.
|
IsMinFilter.add
theorem IsMinFilter.add :
∀ {α : Type u} {β : Type v} [inst : OrderedAddCommMonoid β] {f g : α → β} {a : α} {l : Filter α},
IsMinFilter f l a → IsMinFilter g l a → IsMinFilter (fun x => f x + g x) l a
The theorem `IsMinFilter.add` states that for any types `α` and `β`, where `β` forms an ordered commutative monoid under addition, and any functions `f` and `g` from `α` to `β`, and any `α` value `a` and any filter `l` in `α`, if `a` is a point of minimal value under `f` and under `g` in some `l`-neighborhood, then `a` is also a point of minimal value under the function `h` that maps `x` to `f(x) + g(x)` in the same `l`-neighborhood. In other words, if `f(a)` and `g(a)` are both minimal for all `x` near `a`, then `(f+g)(a)` is also minimal for all `x` near `a`.
More concisely: If `a` minimally satisfies `f(a) = \inf_{x \in l} f(x)` and `g(a) = \inf_{x \in l} g(x)` for some filter `l` and functions `f` and `g` from a type `α` to an ordered commutative monoid `β`, then `a` also minimally satisfies `(f + g)(a) = \inf_{x \in l} (f + g)(x)`.
|
IsMinFilter.comp_tendsto
theorem IsMinFilter.comp_tendsto :
∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {l : Filter α} {g : δ → α} {l' : Filter δ}
{b : δ}, IsMinFilter f l (g b) → Filter.Tendsto g l' l → IsMinFilter (f ∘ g) l' b
The theorem `IsMinFilter.comp_tendsto` states that for any types `α`, `β`, and `δ`, and a preorder on `β`, if `f` is a function from `α` to `β` and `g` is a function from `δ` to `α`, and if `l` is a filter on `α` and `l'` is a filter on `δ`, then if `f` attains a minimum at `g b` for all `α` in the `l`-neighborhood of `g b`, and if `g` tends to `l` along `l'`, then the composition function `f ∘ g` attains a minimum at `b` for all `δ` in the `l'`-neighborhood of `b`.
In simpler words, if `f` has a minimum at the point `g b` under filter `l`, and `g` converges from filter `l'` to `l`, then the composed function `f ∘ g` has a minimum at the point `b` under the filter `l'`.
More concisely: If `f` has a minimum at `g(b)` under filter `l` on `α` and `g` tends to `l` under filter `l'` on `δ`, then `f ∘ g` has a minimum at `b` under filter `l'` on `δ`.
|
IsExtrFilter.filter_mono
theorem IsExtrFilter.filter_mono :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α},
IsExtrFilter f l a → l' ≤ l → IsExtrFilter f l' a
The theorem `IsExtrFilter.filter_mono` states that for all types `α` and `β` with a preorder relation on `β`, for any function `f` from `α` to `β`, for any two filters `l` and `l'` on `α`, and for any element `a` in `α`, if `a` is an extremal value (either a minimum or a maximum) of the function `f` with respect to the filter `l`, and if the filter `l'` is a subfilter of `l`, then `a` is also an extremal value of the function `f` with respect to the filter `l'`. In other words, extremal-ness with respect to a filter is preserved under taking subfilters.
More concisely: If `f` is a function from type `α` to type `β` with a preorder relation, and `a` is an extremal value of `f` with respect to filter `l` on `α`, then `a` is also an extremal value of `f` with respect to any subfilter `l'` of `l`.
|
isExtrFilter_const
theorem isExtrFilter_const :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {a : α} {b : β}, IsExtrFilter (fun x => b) l a := by
sorry
The theorem `isExtrFilter_const` states that for any type `α` and any preorder type `β`, given any filter `l` on `α`, any element `a` from `α`, and any element `b` from `β`, the constant function (which maps every `x` to `b`) is an extreme filter at `a` with respect to `l`. In other words, the constant function either achieves a minimum or a maximum at `a` under the filter `l`.
More concisely: For any filter `l` on type `α`, element `a` from `α`, and element `b` from a preorder type `β`, the constant function from `α` to `β` with value `b` is an extreme filter element at `a` with respect to `l`.
|
IsMaxFilter.comp_mono
theorem IsMaxFilter.comp_mono :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {l : Filter α}
{a : α}, IsMaxFilter f l a → ∀ {g : β → γ}, Monotone g → IsMaxFilter (g ∘ f) l a
The theorem `IsMaxFilter.comp_mono` states that for all types `α`, `β`, and `γ`, if `β` and `γ` have a preorder relation, and if a function `f` from `α` to `β` satisfies the property that `f x` is less than or equal to `f a` for all `x` in some neighborhood of `a` defined by a filter `l` (i.e., `f` is a max filter at `a`), then for any monotone function `g` from `β` to `γ` (i.e., a function where `a ≤ b` implies `f a ≤ f b`), the composition `g ∘ f` is also a max filter at `a`. In other words, the composition of a monotone function and a function that reaches its maximum at `a` still reaches its maximum at `a`.
More concisely: If `f: α → β` is a max filter at `a` in a preorder `β`, and `g: β → γ` is a monotone function, then `g ∘ f` is a max filter at `a` in `γ`.
|
Filter.EventuallyEq.isMinFilter_iff
theorem Filter.EventuallyEq.isMinFilter_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : α → β} {a : α} {l : Filter α},
l.EventuallyEq f g → f a = g a → (IsMinFilter f l a ↔ IsMinFilter g l a)
This theorem states that for any two functions `f` and `g` mapping from a type `α` to a type `β` (where `β` is preordered), a certain point `a` of type `α`, and a filter `l` on `α`, if `f` and `g` become eventually equal at the filter `l` and `f a` equals `g a`, then `f` being a minimum filter at `a` with respect to `l` is equivalent to `g` being a minimum filter at `a` with respect to `l`. In other words, the property of being a minimum filter is preserved under eventual equality at a specific point in the domain.
More concisely: If functions `f` and `g` from type `α` to a preordered type `β` become equal in filter `l` at point `a` where `f a = g a`, then `f` being a minimum filter for `a` with respect to `l` is equivalent to `g` being a minimum filter for `a` with respect to `l`.
|
Filter.EventuallyLE.isMinFilter
theorem Filter.EventuallyLE.isMinFilter :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : α → β} {a : α} {l : Filter α},
l.EventuallyLE f g → f a = g a → IsMinFilter f l a → IsMinFilter g l a
The theorem `Filter.EventuallyLE.isMinFilter` states that for any types `α` and `β`, where `β` has a preorder structure, and any two functions `f` and `g` from `α` to `β`, along with a given filter `l` on `α` and an element `a` of `α`, if `f` is less than or equal to `g` eventually at filter `l` and `f(a)` is equal to `g(a)`, and if `f` has a property of being a minimum filter at `a` (meaning that `f(a)` is less than or equal to `f(x)` for all `x` in some `l`-neighborhood of `a`), then `g` also has the property of being a minimum filter at `a`. In simple terms, under these conditions, if `f` is minimum at `a`, then `g` is also minimum at `a`.
More concisely: If `f` is a minimum filter at `a`, `f(a) ≤ g(a)`, `g(x) ≤ f(x)` for all `x` in some neighborhood of `a` in `α` (i.e., `x ∈ l`), and `f` is eventually less than or equal to `g` at filter `l`, then `g` is a minimum filter at `a`.
|
IsExtrFilter.congr
theorem IsExtrFilter.congr :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : α → β} {a : α} {l : Filter α},
IsExtrFilter f l a → l.EventuallyEq f g → f a = g a → IsExtrFilter g l a
The theorem `IsExtrFilter.congr` states that, for any types `α` and `β` with a preorder structure on `β`, and for any real-valued functions `f` and `g` on `α`, if `f` has an extremum (either a minimum or a maximum) at a point `a` with respect to a filter `l`, and `f` is eventually equal to `g` at `l`, and the values of `f` and `g` at `a` are equal, then `g` also has an extremum at `a` with respect to the same filter `l`. Essentially, this theorem asserts that the property of having an extremum under a certain filter is preserved under eventual equality of functions.
More concisely: If function `f` has an extremum at point `a` with respect to filter `l` in types `α` and `β` with a preorder, and `f` is eventually equal to `g` at `l` and `f(a) = g(a)`, then `g` also has an extremum at `a` with respect to filter `l`.
|
IsMinFilter.filter_mono
theorem IsMinFilter.filter_mono :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α},
IsMinFilter f l a → l' ≤ l → IsMinFilter f l' a
The theorem `IsMinFilter.filter_mono` states that for any types `α` and `β` with a pre-order relation on `β`, a function `f` from `α` to `β`, filters `l` and `l'` on `α`, and an element `a` of type `α`, if `a` is a minimum of the function `f` over the set defined by the filter `l` (that is, for every element `x` in some neighborhood of `a` defined by `l`, the value of `f` at `a` is less than or equal to the value of `f` at `x`), and if the filter `l'` is a subset of `l`, then `a` is also a minimum of the function `f` over the set defined by the filter `l'`.
More concisely: If `a` is a minimum of a function `f` over the filter `l` and `l'` is a subset of `l`, then `a` is also a minimum of `f` over the filter `l'`.
|
IsMinOn.undual
theorem IsMinOn.undual :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMinOn (⇑OrderDual.toDual ∘ f) s a → IsMaxOn f s a
The theorem `IsMinOn.undual` states that for any type `α`, any type `β` with a given preorder structure, any function `f` from `α` to `β`, any set `s` of type `α`, and any element `a` of type `α`, if `a` is a minimum of the function `f` composed with the identity function to the `OrderDual` of `β` on the set `s`, then `a` is a maximum of the function `f` on the set `s`. In other words, finding a minimum in the order dual is equivalent to finding a maximum in the original order. The `OrderDual` of a type is like flipping the ordering of the elements, so the smallest element in the order dual is the largest in the original order.
More concisely: If `a` is the minimum of `f` composed with the order dual function on set `s`, then `a` is the maximum of `f` on `s`.
|
IsMinFilter.comp_mono
theorem IsMinFilter.comp_mono :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {l : Filter α}
{a : α}, IsMinFilter f l a → ∀ {g : β → γ}, Monotone g → IsMinFilter (g ∘ f) l a
The theorem `IsMinFilter.comp_mono` states that for all types `α`, `β`, `γ` with a preorder on `β` and `γ`, and for any function `f` from `α` to `β`, a filter `l` on `α`, and an element `a` of type `α`, if `f` has a property that it reaches its minimum at `a` for all elements `x` in some `l`-neighborhood of `a`, then for any monotone function `g` from `β` to `γ`, the function composed of `g` and `f` (i.e., `g ∘ f`) also has the property that it reaches its minimum at `a` for all elements `x` in the same `l`-neighborhood of `a`. Here, a function `g` is considered monotone if for all `a` and `b` such that `a ≤ b`, we have `g(a) ≤ g(b)`.
More concisely: Given types `α`, `β`, `γ` with preorders, a filter `l` on `α`, a function `f: α → β`, an element `a ∈ α`, and monotone function `g: β → γ`, if `f` minimizes at `a` in some `l`-neighborhood, then `g ∘ f` also minimizes at `a` in the same `l`-neighborhood.
|
Filter.EventuallyEq.isMaxFilter_iff
theorem Filter.EventuallyEq.isMaxFilter_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : α → β} {a : α} {l : Filter α},
l.EventuallyEq f g → f a = g a → (IsMaxFilter f l a ↔ IsMaxFilter g l a)
The theorem `Filter.EventuallyEq.isMaxFilter_iff` states that for all types `α` and `β`, where `β` is a Preorder, for any functions `f` and `g` from `α` to `β`, any element `a` of type `α`, and any filter `l` on `α`, if `f` and `g` are eventually equal at the filter `l` and `f a` equals `g a`, then `f` is a maximal filter at `a` with respect to `l` if and only if `g` is also a maximal filter at `a` with respect to `l`. In other words, if two functions are the same in a neighborhood of `a` and agree at `a`, they share the same maxima in that neighborhood.
More concisely: For functions `f` and `g` from type `α` to a preordered type `β`, and for an element `a` of type `α` and a filter `l` on `α`, if `f` and `g` are eventually equal at `l` and agree at `a`, then `f` and `g` have the same maximal elements at `a` with respect to `l`.
|
IsMinFilter.undual
theorem IsMinFilter.undual :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter (⇑OrderDual.toDual ∘ f) l a → IsMaxFilter f l a
The theorem `IsMinFilter.undual` states that for any types `α` and `β` with `β` being a preorder, any function `f` from `α` to `β`, any filter `l` on `α`, and any element `a` in `α`, if `f` composed with the identity function to the order dual (i.e., `⇑OrderDual.toDual ∘ f`) is a minimum filter at `a` for some `l`-neighborhood of `a`, then `f` itself is a maximum filter at `a` for the same `l`-neighborhood. In simpler terms, it shows a correspondence between the concepts of minimum filters with a function and maximum filters with its dual function under a certain condition.
More concisely: If a function `f` from type `α` to a preordered type `β` has its dual function `OrderDual.toDual �circ f` being a minimum filter at `a` in some filter `l` on `α`, then `f` is a maximum filter at `a` for the same `l`-neighborhood.
|
IsMaxFilter.dual
theorem IsMaxFilter.dual :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter f l a → IsMinFilter (⇑OrderDual.toDual ∘ f) l a
The theorem `IsMaxFilter.dual` states that for any types `α` and `β`, any function `f` from `α` to `β`, any filter `l` on `α`, and any element `a` of `α`, if `f` achieves its maximum value at `a` in some `l`-neighborhood, then `f` achieves its minimum value at `a` in the same `l`-neighborhood when the order of `β` is reversed. Here, `IsMaxFilter f l a` means `f` is maximized at `a` in some `l`-neighborhood, `IsMinFilter (⇑OrderDual.toDual ∘ f) l a` means `f`, under the reversed order, is minimized at `a` in some `l`-neighborhood, and `⇑OrderDual.toDual` is the identity function that reverses the order, turning a maximum into a minimum.
More concisely: If a function `f` from type `α` to type `β` attains a maximum value at an element `a` in the neighborhood of a filter `l` on `α`, then `f` attains a minimum value at `a` in the same neighborhood under the reversed order on `β`.
|