Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Yury Kudryashov

! This file was ported from Lean 3 source module order.filter.extr
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.Filter.Basic
import Mathlib.Order.ConditionallyCompleteLattice.Basic

/-!
# Minimum and maximum w.r.t. a filter and on a aet

## Main Definitions

This file defines six predicates of the form `isAB`, where `A` is `Min`, `Max`, or `Extr`,
and `B` is `Filter` or `On`.

* `isMinFilter f l a` means that `f a ≤ f x` in some `l`-neighborhood of `a`;
* `isMaxFilter f l a` means that `f x ≤ f a` in some `l`-neighborhood of `a`;
* `isExtrFilter f l a` means `isMinFilter f l a` or `isMaxFilter f l a`.

Similar predicates with `on` suffix are particular cases for `l = 𝓟 s`.

## Main statements

### Change of the filter (set) argument

* `is*Filter.filter_mono` : replace the filter with a smaller one;
* `is*Filter.filter_inf` : replace a filter `l` with `l ⊓ l'`;
* `is*On.on_subset` : restrict to a smaller set;
* `is*Pn.inter` : replace a set `s` wtih `s ∩ t`.

### Composition

* `is**.comp_mono` : if `x` is an extremum for `f` and `g` is a monotone function,
then `x` is an extremum for `g ∘ f`;
* `is**.comp_antitone` : similarly for the case of antitone `g`;
* `is**.bicomp_mono` : if `x` is an extremum of the same type for `f` and `g`
and a binary operation `op` is monotone in both arguments, then `x` is an extremum
of the same type for `fun x => op (f x) (g x)`.
* `is*Filter.comp_tendsto` : if `g x` is an extremum for `f` w.r.t. `l'` and `Tendsto g l l'`,
then `x` is an extremum for `f ∘ g` w.r.t. `l`.
* `is*On.on_preimage` : if `g x` is an extremum for `f` on `s`, then `x` is an extremum
for `f ∘ g` on `g ⁻¹' s`.

### Algebraic operations

* `is**.add` : if `x` is an extremum of the same type for two functions,
then it is an extremum of the same type for their sum;
* `is**.neg` : if `x` is an extremum for `f`, then it is an extremum
of the opposite type for `-f`;
* `is**.sub` : if `x` is an a minimum for `f` and a maximum for `g`,
then it is a minimum for `f - g` and a maximum for `g - f`;
* `is**.max`, `is**.min`, `is**.sup`, `is**.inf` : similarly for `is**.add`
for pointwise `max`, `min`, `sup`, `inf`, respectively.

### Miscellaneous definitions

* `is**_const` : any point is both a minimum and maximum for a constant function;
* `isMin/Max*.isExt` : any minimum/maximum point is an extremum;
* `is**.dual`, `is**.undual`: conversion between codomains `α` and `dual α`;

## Missing features (TODO)

* Multiplication and division;
* `is**.bicompl` : if `x` is a minimum for `f`, `y` is a minimum for `g`, and `op` is a monotone
binary operation, then `(x, y)` is a minimum for `uncurry (bicompl op f g)`. From this point
of view, `is**.bicomp` is a composition
* It would be nice to have a tactic that specializes `comp_(anti)mono` or `bicomp_mono`
based on a proof of monotonicity of a given (binary) function. The tactic should maintain a `meta`
list of known (anti)monotone (binary) functions with their names, as well as a list of special
types of filters, and define the missing lemmas once one of these two lists grows.
-/

universe u v w x

variable {α: Type uα : Type u: Type (u+1)Type u} {β: Type vβ : Type v: Type (v+1)Type v} {γ: Type wγ : Type w: Type (w+1)Type w} {δ: Type xδ : Type x: Type (x+1)Type x}

open Set Filter

open Filter

section Preorder

variable [Preorder: Type ?u.918 → Type ?u.918Preorder β: Type vβ] [Preorder: Type ?u.2533 → Type ?u.2533Preorder γ: Type wγ]

variable (f: α → βf : α: Type uα → β: Type vβ) (s: Set αs : Set: Type ?u.4060 → Type ?u.4060Set α: Type uα) (l: Filter αl : Filter: Type ?u.1565 → Type ?u.1565Filter α: Type uα) (a: αa : α: Type uα)

/-! ### Definitions -/

/-- `IsMinFilter f l a` means that `f a ≤ f x` in some `l`-neighborhood of `a` -/
def IsMinFilter: PropIsMinFilter : Prop: TypeProp :=
∀ᶠ x: ?m.80x in l: Filter αl, f: α → βf a: αa ≤ f: α → βf x: ?m.80x
#align is_min_filter IsMinFilter: {α : Type u} → {β : Type v} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter

/-- `is_maxFilter f l a` means that `f x ≤ f a` in some `l`-neighborhood of `a` -/
def IsMaxFilter: PropIsMaxFilter : Prop: TypeProp :=
∀ᶠ x: ?m.145x in l: Filter αl, f: α → βf x: ?m.145x ≤ f: α → βf a: αa
#align is_max_filter IsMaxFilter: {α : Type u} → {β : Type v} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter

/-- `IsExtrFilter f l a` means `IsMinFilter f l a` or `IsMaxFilter f l a` -/
def IsExtrFilter: PropIsExtrFilter : Prop: TypeProp :=
IsMinFilter: {α : Type ?u.208} → {β : Type ?u.207} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter f: α → βf l: Filter αl a: αa ∨ IsMaxFilter: {α : Type ?u.221} → {β : Type ?u.220} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter f: α → βf l: Filter αl a: αa
#align is_extr_filter IsExtrFilter: {α : Type u} → {β : Type v} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsExtrFilter

/-- `IsMinOn f s a` means that `f a ≤ f x` for all `x ∈ a`. Note that we do not assume `a ∈ s`. -/
def IsMinOn: {α : Type u} → {β : Type v} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn :=
IsMinFilter: {α : Type ?u.272} → {β : Type ?u.271} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter f: α → βf (𝓟: Set ?m.302 → Filter ?m.302𝓟 s: Set αs) a: αa
#align is_min_on IsMinOn: {α : Type u} → {β : Type v} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn

/-- `IsMaxOn f s a` means that `f x ≤ f a` for all `x ∈ a`. Note that we do not assume `a ∈ s`. -/
def IsMaxOn: ?m.352IsMaxOn :=
IsMaxFilter: {α : Type ?u.355} → {β : Type ?u.354} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter f: α → βf (𝓟: Set ?m.385 → Filter ?m.385𝓟 s: Set αs) a: αa
#align is_max_on IsMaxOn: {α : Type u} → {β : Type v} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn

/-- `IsExtrOn f s a` means `IsMinOn f s a` or `IsMaxOn f s a` -/
def IsExtrOn: PropIsExtrOn : Prop: TypeProp :=
IsExtrFilter: {α : Type ?u.437} → {β : Type ?u.436} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsExtrFilter f: α → βf (𝓟: Set ?m.445 → Filter ?m.445𝓟 s: Set αs) a: αa
#align is_extr_on IsExtrOn: {α : Type u} → {β : Type v} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn

variable {f: ?m.495f s: ?m.498s a: ?m.501a l: ?m.504l} {t: Set αt : Set: Type ?u.2548 → Type ?u.2548Set α: Type uα} {l': Filter αl' : Filter: Type ?u.12829 → Type ?u.12829Filter α: Type uα}

theorem IsExtrOn.elim: ∀ {p : Prop}, IsExtrOn f s a → (IsMinOn f s a → p) → (IsMaxOn f s a → p) → pIsExtrOn.elim {p: Propp : Prop: TypeProp} : IsExtrOn: {α : Type ?u.549} → {β : Type ?u.548} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn f: α → βf s: Set αs a: αa → (IsMinOn: {α : Type ?u.588} → {β : Type ?u.587} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn f: α → βf s: Set αs a: αa → p: Propp) → (IsMaxOn: {α : Type ?u.623} → {β : Type ?u.622} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn f: α → βf s: Set αs a: αa → p: Propp) → p: Propp :=
Or.elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → cOr.elim
#align is_extr_on.elim 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) → pIsExtrOn.elim

theorem isMinOn_iff: IsMinOn f s a ↔ ∀ (x : α), x ∈ s → f a ≤ f xisMinOn_iff : IsMinOn: {α : Type ?u.717} → {β : Type ?u.716} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn f: α → βf s: Set αs a: αa ↔ ∀ x: ?m.731x ∈ s: Set αs, f: α → βf a: αa ≤ f: α → βf x: ?m.731x :=
Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl
#align is_min_on_iff isMinOn_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMinOn f s a ↔ ∀ (x : α), x ∈ s → f a ≤ f xisMinOn_iff

theorem isMaxOn_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMaxOn f s a ↔ ∀ (x : α), x ∈ s → f x ≤ f aisMaxOn_iff : IsMaxOn: {α : Type ?u.830} → {β : Type ?u.829} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn f: α → βf s: Set αs a: αa ↔ ∀ x: ?m.844x ∈ s: Set αs, f: α → βf x: ?m.844x ≤ f: α → βf a: αa :=
Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl
#align is_max_on_iff isMaxOn_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMaxOn f s a ↔ ∀ (x : α), x ∈ s → f x ≤ f aisMaxOn_iff

theorem isMinOn_univ_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {a : α}, IsMinOn f univ a ↔ ∀ (x : α), f a ≤ f xisMinOn_univ_iff : IsMinOn: {α : Type ?u.943} → {β : Type ?u.942} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn f: α → βf univ: {α : Type ?u.950} → Set αuniv a: αa ↔ ∀ x: ?m.959x, f: α → βf a: αa ≤ f: α → βf x: ?m.959x :=
univ_subset_iff: ∀ {α : Type ?u.975} {s : Set α}, univ ⊆ s ↔ s = univuniv_subset_iff.trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)trans eq_univ_iff_forall: ∀ {α : Type ?u.996} {s : Set α}, s = univ ↔ ∀ (x : α), x ∈ seq_univ_iff_forall
#align is_min_on_univ_iff isMinOn_univ_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {a : α}, IsMinOn f univ a ↔ ∀ (x : α), f a ≤ f xisMinOn_univ_iff

theorem isMaxOn_univ_iff: IsMaxOn f univ a ↔ ∀ (x : α), f x ≤ f aisMaxOn_univ_iff : IsMaxOn: {α : Type ?u.1049} → {β : Type ?u.1048} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn f: α → βf univ: {α : Type ?u.1056} → Set αuniv a: αa ↔ ∀ x: ?m.1065x, f: α → βf x: ?m.1065x ≤ f: α → βf a: αa :=
univ_subset_iff: ∀ {α : Type ?u.1081} {s : Set α}, univ ⊆ s ↔ s = univuniv_subset_iff.trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)trans eq_univ_iff_forall: ∀ {α : Type ?u.1102} {s : Set α}, s = univ ↔ ∀ (x : α), x ∈ seq_univ_iff_forall
#align is_max_on_univ_iff isMaxOn_univ_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {a : α}, IsMaxOn f univ a ↔ ∀ (x : α), f x ≤ f aisMaxOn_univ_iff

theorem IsMinFilter.tendsto_principal_Ici: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter f l a → Tendsto f l (𝓟 (Ici (f a)))IsMinFilter.tendsto_principal_Ici (h: IsMinFilter f l ah : IsMinFilter: {α : Type ?u.1155} → {β : Type ?u.1154} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter f: α → βf l: Filter αl a: αa) : Tendsto: {α : Type ?u.1192} → {β : Type ?u.1191} → (α → β) → Filter α → Filter β → PropTendsto f: α → βf l: Filter αl (𝓟: Set ?m.1199 → Filter ?m.1199𝓟 <| Ici: {α : Type ?u.1202} → [inst : Preorder α] → α → Set αIci (f: α → βf a: αa)) :=
tendsto_principal: ∀ {α : Type ?u.1234} {β : Type ?u.1233} {f : α → β} {l : Filter α} {s : Set β},
Tendsto f l (𝓟 s) ↔ Filter.Eventually (fun a => f a ∈ s) ltendsto_principal.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 h: IsMinFilter f l ah
#align is_min_filter.tendsto_principal_Ici IsMinFilter.tendsto_principal_Ici: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter f l a → Tendsto f l (𝓟 (Ici (f a)))IsMinFilter.tendsto_principal_Ici

theorem IsMaxFilter.tendsto_principal_Iic: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter f l a → Tendsto f l (𝓟 (Iic (f a)))IsMaxFilter.tendsto_principal_Iic (h: IsMaxFilter f l ah : IsMaxFilter: {α : Type ?u.1308} → {β : Type ?u.1307} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter f: α → βf l: Filter αl a: αa) : Tendsto: {α : Type ?u.1345} → {β : Type ?u.1344} → (α → β) → Filter α → Filter β → PropTendsto f: α → βf l: Filter αl (𝓟: Set ?m.1352 → Filter ?m.1352𝓟 <| Iic: {α : Type ?u.1355} → [inst : Preorder α] → α → Set αIic (f: α → βf a: αa)) :=
tendsto_principal: ∀ {α : Type ?u.1387} {β : Type ?u.1386} {f : α → β} {l : Filter α} {s : Set β},
Tendsto f l (𝓟 s) ↔ Filter.Eventually (fun a => f a ∈ s) ltendsto_principal.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 h: IsMaxFilter f l ah
#align is_max_filter.tendsto_principal_Iic IsMaxFilter.tendsto_principal_Iic: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter f l a → Tendsto f l (𝓟 (Iic (f a)))IsMaxFilter.tendsto_principal_Iic

/-! ### Conversion to `IsExtr*` -/

theorem IsMinFilter.isExtr: IsMinFilter f l a → IsExtrFilter f l aIsMinFilter.isExtr : IsMinFilter: {α : Type ?u.1462} → {β : Type ?u.1461} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter f: α → βf l: Filter αl a: αa → IsExtrFilter: {α : Type ?u.1498} → {β : Type ?u.1497} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsExtrFilter f: α → βf l: Filter αl a: αa :=
Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl
#align is_min_filter.is_extr IsMinFilter.isExtr: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter f l a → IsExtrFilter f l aIsMinFilter.isExtr

theorem IsMaxFilter.isExtr: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter f l a → IsExtrFilter f l aIsMaxFilter.isExtr : IsMaxFilter: {α : Type ?u.1578} → {β : Type ?u.1577} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter f: α → βf l: Filter αl a: αa → IsExtrFilter: {α : Type ?u.1614} → {β : Type ?u.1613} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsExtrFilter f: α → βf l: Filter αl a: αa :=
Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr
#align is_max_filter.is_extr IsMaxFilter.isExtr: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter f l a → IsExtrFilter f l aIsMaxFilter.isExtr

theorem IsMinOn.isExtr: IsMinOn f s a → IsExtrOn f s aIsMinOn.isExtr (h: IsMinOn f s ah : IsMinOn: {α : Type ?u.1693} → {β : Type ?u.1692} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn f: α → βf s: Set αs a: αa) : IsExtrOn: {α : Type ?u.1731} → {β : Type ?u.1730} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn f: α → βf s: Set αs a: αa :=
IsMinFilter.isExtr: ∀ {α : Type ?u.1765} {β : Type ?u.1764} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter f l a → IsExtrFilter f l aIsMinFilter.isExtr h: IsMinOn f s ah
#align is_min_on.is_extr IsMinOn.isExtr: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α}, IsMinOn f s a → IsExtrOn f s aIsMinOn.isExtr

theorem IsMaxOn.isExtr: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α}, IsMaxOn f s a → IsExtrOn f s aIsMaxOn.isExtr (h: IsMaxOn f s ah : IsMaxOn: {α : Type ?u.1845} → {β : Type ?u.1844} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn f: α → βf s: Set αs a: αa) : IsExtrOn: {α : Type ?u.1883} → {β : Type ?u.1882} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn f: α → βf s: Set αs a: αa :=
IsMaxFilter.isExtr: ∀ {α : Type ?u.1917} {β : Type ?u.1916} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter f l a → IsExtrFilter f l aIsMaxFilter.isExtr h: IsMaxOn f s ah
#align is_max_on.is_extr IsMaxOn.isExtr: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α}, IsMaxOn f s a → IsExtrOn f s aIsMaxOn.isExtr

/-! ### Constant function -/

theorem isMinFilter_const: ∀ {b : β}, IsMinFilter (fun x => b) l aisMinFilter_const {b: βb : β: Type vβ} : IsMinFilter: {α : Type ?u.1999} → {β : Type ?u.1998} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter (fun _: ?m.2026_ => b: βb) l: Filter αl a: αa :=
univ_mem': ∀ {α : Type ?u.2039} {f : Filter α} {s : Set α}, (∀ (a : α), a ∈ s) → s ∈ funiv_mem' fun _: ?m.2052_ => le_rfl: ∀ {α : Type ?u.2054} [inst : Preorder α] {a : α}, a ≤ ale_rfl
#align is_min_filter_const isMinFilter_const: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {a : α} {b : β}, IsMinFilter (fun x => b) l aisMinFilter_const

theorem isMaxFilter_const: ∀ {b : β}, IsMaxFilter (fun x => b) l aisMaxFilter_const {b: βb : β: Type vβ} : IsMaxFilter: {α : Type ?u.2133} → {β : Type ?u.2132} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter (fun _: ?m.2160_ => b: βb) l: Filter αl a: αa :=
univ_mem': ∀ {α : Type ?u.2173} {f : Filter α} {s : Set α}, (∀ (a : α), a ∈ s) → s ∈ funiv_mem' fun _: ?m.2186_ => le_rfl: ∀ {α : Type ?u.2188} [inst : Preorder α] {a : α}, a ≤ ale_rfl
#align is_max_filter_const isMaxFilter_const: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {a : α} {b : β}, IsMaxFilter (fun x => b) l aisMaxFilter_const

theorem isExtrFilter_const: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {a : α} {b : β}, IsExtrFilter (fun x => b) l aisExtrFilter_const {b: βb : β: Type vβ} : IsExtrFilter: {α : Type ?u.2267} → {β : Type ?u.2266} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsExtrFilter (fun _: ?m.2294_ => b: βb) l: Filter αl a: αa :=
isMinFilter_const: ∀ {α : Type ?u.2308} {β : Type ?u.2307} [inst : Preorder β] {l : Filter α} {a : α} {b : β}, IsMinFilter (fun x => b) l aisMinFilter_const.isExtr: ∀ {α : Type ?u.2338} {β : Type ?u.2337} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter f l a → IsExtrFilter f l aisExtr
#align is_extr_filter_const isExtrFilter_const: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {a : α} {b : β}, IsExtrFilter (fun x => b) l aisExtrFilter_const

theorem isMinOn_const: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {s : Set α} {a : α} {b : β}, IsMinOn (fun x => b) s aisMinOn_const {b: βb : β: Type vβ} : IsMinOn: {α : Type ?u.2435} → {β : Type ?u.2434} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn (fun _: ?m.2462_ => b: βb) s: Set αs a: αa :=
isMinFilter_const: ∀ {α : Type ?u.2477} {β : Type ?u.2476} [inst : Preorder β] {l : Filter α} {a : α} {b : β}, IsMinFilter (fun x => b) l aisMinFilter_const
#align is_min_on_const isMinOn_const: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {s : Set α} {a : α} {b : β}, IsMinOn (fun x => b) s aisMinOn_const

theorem isMaxOn_const: ∀ {b : β}, IsMaxOn (fun x => b) s aisMaxOn_const {b: βb : β: Type vβ} : IsMaxOn: {α : Type ?u.2557} → {β : Type ?u.2556} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn (fun _: ?m.2584_ => b: βb) s: Set αs a: αa :=
isMaxFilter_const: ∀ {α : Type ?u.2599} {β : Type ?u.2598} [inst : Preorder β] {l : Filter α} {a : α} {b : β}, IsMaxFilter (fun x => b) l aisMaxFilter_const
#align is_max_on_const isMaxOn_const: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {s : Set α} {a : α} {b : β}, IsMaxOn (fun x => b) s aisMaxOn_const

theorem isExtrOn_const: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {s : Set α} {a : α} {b : β}, IsExtrOn (fun x => b) s aisExtrOn_const {b: βb : β: Type vβ} : IsExtrOn: {α : Type ?u.2679} → {β : Type ?u.2678} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn (fun _: ?m.2706_ => b: βb) s: Set αs a: αa :=
isExtrFilter_const: ∀ {α : Type ?u.2721} {β : Type ?u.2720} [inst : Preorder β] {l : Filter α} {a : α} {b : β},
IsExtrFilter (fun x => b) l aisExtrFilter_const
#align is_extr_on_const isExtrOn_const: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {s : Set α} {a : α} {b : β}, IsExtrOn (fun x => b) s aisExtrOn_const

/-! ### Order dual -/

open OrderDual (toDual)

theorem isMinFilter_dual_iff: IsMinFilter (↑toDual ∘ f) l a ↔ IsMaxFilter f l aisMinFilter_dual_iff : IsMinFilter: {α : Type ?u.2799} → {β : Type ?u.2798} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter (toDual: {α : Type ?u.2811} → α ≃ αᵒᵈtoDual ∘ f: α → βf) l: Filter αl a: αa ↔ IsMaxFilter: {α : Type ?u.2921} → {β : Type ?u.2920} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter f: α → βf l: Filter αl a: αa :=
Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl
#align is_min_filter_dual_iff isMinFilter_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter (↑toDual ∘ f) l a ↔ IsMaxFilter f l aisMinFilter_dual_iff

theorem isMaxFilter_dual_iff: IsMaxFilter (↑toDual ∘ f) l a ↔ IsMinFilter f l aisMaxFilter_dual_iff : IsMaxFilter: {α : Type ?u.2985} → {β : Type ?u.2984} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter (toDual: {α : Type ?u.2997} → α ≃ αᵒᵈtoDual ∘ f: α → βf) l: Filter αl a: αa ↔ IsMinFilter: {α : Type ?u.3107} → {β : Type ?u.3106} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter f: α → βf l: Filter αl a: αa :=
Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl
#align is_max_filter_dual_iff isMaxFilter_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter (↑toDual ∘ f) l a ↔ IsMinFilter f l aisMaxFilter_dual_iff

theorem isExtrFilter_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsExtrFilter (↑toDual ∘ f) l a ↔ IsExtrFilter f l aisExtrFilter_dual_iff : IsExtrFilter: {α : Type ?u.3171} → {β : Type ?u.3170} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsExtrFilter (toDual: {α : Type ?u.3183} → α ≃ αᵒᵈtoDual ∘ f: α → βf) l: Filter αl a: αa ↔ IsExtrFilter: {α : Type ?u.3293} → {β : Type ?u.3292} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsExtrFilter f: α → βf l: Filter αl a: αa :=
or_comm: ∀ {a b : Prop}, a ∨ b ↔ b ∨ aor_comm
#align is_extr_filter_dual_iff isExtrFilter_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsExtrFilter (↑toDual ∘ f) l a ↔ IsExtrFilter f l aisExtrFilter_dual_iff

alias isMinFilter_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter (↑toDual ∘ f) l a ↔ IsMaxFilter f l aisMinFilter_dual_iff ↔ IsMinFilter.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter (↑toDual ∘ f) l a → IsMaxFilter f l aIsMinFilter.undual IsMaxFilter.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter f l a → IsMinFilter (↑toDual ∘ f) l aIsMaxFilter.dual
#align is_min_filter.undual IsMinFilter.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter (↑toDual ∘ f) l a → IsMaxFilter f l aIsMinFilter.undual
#align is_max_filter.dual IsMaxFilter.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter f l a → IsMinFilter (↑toDual ∘ f) l aIsMaxFilter.dual

alias isMaxFilter_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter (↑toDual ∘ f) l a ↔ IsMinFilter f l aisMaxFilter_dual_iff ↔ IsMaxFilter.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter (↑toDual ∘ f) l a → IsMinFilter f l aIsMaxFilter.undual IsMinFilter.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter f l a → IsMaxFilter (↑toDual ∘ f) l aIsMinFilter.dual
#align is_max_filter.undual IsMaxFilter.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter (↑toDual ∘ f) l a → IsMinFilter f l aIsMaxFilter.undual
#align is_min_filter.dual IsMinFilter.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter f l a → IsMaxFilter (↑toDual ∘ f) l aIsMinFilter.dual

alias isExtrFilter_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsExtrFilter (↑toDual ∘ f) l a ↔ IsExtrFilter f l aisExtrFilter_dual_iff ↔ IsExtrFilter.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsExtrFilter (↑toDual ∘ f) l a → IsExtrFilter f l aIsExtrFilter.undual IsExtrFilter.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsExtrFilter f l a → IsExtrFilter (↑toDual ∘ f) l aIsExtrFilter.dual
#align is_extr_filter.undual IsExtrFilter.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsExtrFilter (↑toDual ∘ f) l a → IsExtrFilter f l aIsExtrFilter.undual
#align is_extr_filter.dual IsExtrFilter.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsExtrFilter f l a → IsExtrFilter (↑toDual ∘ f) l aIsExtrFilter.dual

theorem isMinOn_dual_iff: IsMinOn (↑toDual ∘ f) s a ↔ IsMaxOn f s aisMinOn_dual_iff : IsMinOn: {α : Type ?u.3434} → {β : Type ?u.3433} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn (toDual: {α : Type ?u.3446} → α ≃ αᵒᵈtoDual ∘ f: α → βf) s: Set αs a: αa ↔ IsMaxOn: {α : Type ?u.3557} → {β : Type ?u.3556} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn f: α → βf s: Set αs a: αa :=
Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl
#align is_min_on_dual_iff isMinOn_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMinOn (↑toDual ∘ f) s a ↔ IsMaxOn f s aisMinOn_dual_iff

theorem isMaxOn_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMaxOn (↑toDual ∘ f) s a ↔ IsMinOn f s aisMaxOn_dual_iff : IsMaxOn: {α : Type ?u.3622} → {β : Type ?u.3621} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn (toDual: {α : Type ?u.3634} → α ≃ αᵒᵈtoDual ∘ f: α → βf) s: Set αs a: αa ↔ IsMinOn: {α : Type ?u.3745} → {β : Type ?u.3744} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn f: α → βf s: Set αs a: αa :=
Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl
#align is_max_on_dual_iff isMaxOn_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMaxOn (↑toDual ∘ f) s a ↔ IsMinOn f s aisMaxOn_dual_iff

theorem isExtrOn_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsExtrOn (↑toDual ∘ f) s a ↔ IsExtrOn f s aisExtrOn_dual_iff : IsExtrOn: {α : Type ?u.3810} → {β : Type ?u.3809} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn (toDual: {α : Type ?u.3822} → α ≃ αᵒᵈtoDual ∘ f: α → βf) s: Set αs a: αa ↔ IsExtrOn: {α : Type ?u.3933} → {β : Type ?u.3932} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn f: α → βf s: Set αs a: αa :=
or_comm: ∀ {a b : Prop}, a ∨ b ↔ b ∨ aor_comm
#align is_extr_on_dual_iff isExtrOn_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsExtrOn (↑toDual ∘ f) s a ↔ IsExtrOn f s aisExtrOn_dual_iff

alias isMinOn_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMinOn (↑toDual ∘ f) s a ↔ IsMaxOn f s aisMinOn_dual_iff ↔ IsMinOn.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMinOn (↑toDual ∘ f) s a → IsMaxOn f s aIsMinOn.undual IsMaxOn.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMaxOn f s a → IsMinOn (↑toDual ∘ f) s aIsMaxOn.dual
#align is_min_on.undual IsMinOn.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMinOn (↑toDual ∘ f) s a → IsMaxOn f s aIsMinOn.undual
#align is_max_on.dual IsMaxOn.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMaxOn f s a → IsMinOn (↑toDual ∘ f) s aIsMaxOn.dual

alias isMaxOn_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMaxOn (↑toDual ∘ f) s a ↔ IsMinOn f s aisMaxOn_dual_iff ↔ IsMaxOn.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMaxOn (↑toDual ∘ f) s a → IsMinOn f s aIsMaxOn.undual IsMinOn.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMinOn f s a → IsMaxOn (↑toDual ∘ f) s aIsMinOn.dual
#align is_max_on.undual IsMaxOn.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMaxOn (↑toDual ∘ f) s a → IsMinOn f s aIsMaxOn.undual
#align is_min_on.dual IsMinOn.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMinOn f s a → IsMaxOn (↑toDual ∘ f) s aIsMinOn.dual

alias isExtrOn_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsExtrOn (↑toDual ∘ f) s a ↔ IsExtrOn f s aisExtrOn_dual_iff ↔ IsExtrOn.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsExtrOn (↑toDual ∘ f) s a → IsExtrOn f s aIsExtrOn.undual IsExtrOn.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsExtrOn f s a → IsExtrOn (↑toDual ∘ f) s aIsExtrOn.dual
#align is_extr_on.undual IsExtrOn.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsExtrOn (↑toDual ∘ f) s a → IsExtrOn f s aIsExtrOn.undual
#align is_extr_on.dual IsExtrOn.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsExtrOn f s a → IsExtrOn (↑toDual ∘ f) s aIsExtrOn.dual

/-! ### Operations on the filter/set -/

theorem IsMinFilter.filter_mono: IsMinFilter f l a → l' ≤ l → IsMinFilter f l' aIsMinFilter.filter_mono (h: IsMinFilter f l ah : IsMinFilter: {α : Type ?u.4075} → {β : Type ?u.4074} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter f: α → βf l: Filter αl a: αa) (hl: l' ≤ lhl : l': Filter αl' ≤ l: Filter αl) : IsMinFilter: {α : Type ?u.4148} → {β : Type ?u.4147} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter f: α → βf l': Filter αl' a: αa :=
hl: l' ≤ lhl h: IsMinFilter f l ah
#align is_min_filter.filter_mono IsMinFilter.filter_mono: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α},
IsMinFilter f l a → l' ≤ l → IsMinFilter f l' aIsMinFilter.filter_mono

theorem IsMaxFilter.filter_mono: IsMaxFilter f l a → l' ≤ l → IsMaxFilter f l' aIsMaxFilter.filter_mono (h: IsMaxFilter f l ah : IsMaxFilter: {α : Type ?u.4234} → {β : Type ?u.4233} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter f: α → βf l: Filter αl a: αa) (hl: l' ≤ lhl : l': Filter αl' ≤ l: Filter αl) : IsMaxFilter: {α : Type ?u.4307} → {β : Type ?u.4306} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter f: α → βf l': Filter αl' a: αa :=
hl: l' ≤ lhl h: IsMaxFilter f l ah
#align is_max_filter.filter_mono IsMaxFilter.filter_mono: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α},
IsMaxFilter f l a → l' ≤ l → IsMaxFilter f l' aIsMaxFilter.filter_mono

theorem IsExtrFilter.filter_mono: IsExtrFilter f l a → l' ≤ l → IsExtrFilter f l' aIsExtrFilter.filter_mono (h: IsExtrFilter f l ah : IsExtrFilter: {α : Type ?u.4393} → {β : Type ?u.4392} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsExtrFilter f: α → βf l: Filter αl a: αa) (hl: l' ≤ lhl : l': Filter αl' ≤ l: Filter αl) : IsExtrFilter: {α : Type ?u.4466} → {β : Type ?u.4465} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsExtrFilter f: α → βf l': Filter αl' a: αa :=
h: IsExtrFilter f l ah.elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → celim (fun h: ?m.4512h => (h: ?m.4512h.filter_mono: ∀ {α : Type ?u.4515} {β : Type ?u.4514} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α},
IsMinFilter f l a → l' ≤ l → IsMinFilter f l' afilter_mono hl: l' ≤ lhl).isExtr: ∀ {α : Type ?u.4545} {β : Type ?u.4544} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter f l a → IsExtrFilter f l aisExtr) fun h: ?m.4570h => (h: ?m.4570h.filter_mono: ∀ {α : Type ?u.4573} {β : Type ?u.4572} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α},
IsMaxFilter f l a → l' ≤ l → IsMaxFilter f l' afilter_mono hl: l' ≤ lhl).isExtr: ∀ {α : Type ?u.4599} {β : Type ?u.4598} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter f l a → IsExtrFilter f l aisExtr
#align is_extr_filter.filter_mono IsExtrFilter.filter_mono: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α},
IsExtrFilter f l a → l' ≤ l → IsExtrFilter f l' aIsExtrFilter.filter_mono

theorem IsMinFilter.filter_inf: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter f l a → ∀ (l' : Filter α), IsMinFilter f (l ⊓ l') aIsMinFilter.filter_inf (h: IsMinFilter f l ah : IsMinFilter: {α : Type ?u.4662} → {β : Type ?u.4661} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter f: α → βf l: Filter αl a: αa) (l': Filter αl') : IsMinFilter: {α : Type ?u.4702} → {β : Type ?u.4701} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter f: α → βf (l: Filter αl ⊓ l': ?m.4698l') a: αa :=
h: IsMinFilter f l ah.filter_mono: ∀ {α : Type ?u.4768} {β : Type ?u.4767} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α},
IsMinFilter f l a → l' ≤ l → IsMinFilter f l' afilter_mono inf_le_left: ∀ {α : Type ?u.4793} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ ainf_le_left
#align is_min_filter.filter_inf IsMinFilter.filter_inf: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter f l a → ∀ (l' : Filter α), IsMinFilter f (l ⊓ l') aIsMinFilter.filter_inf

theorem IsMaxFilter.filter_inf: IsMaxFilter f l a → ∀ (l' : Filter α), IsMaxFilter f (l ⊓ l') aIsMaxFilter.filter_inf (h: IsMaxFilter f l ah : IsMaxFilter: {α : Type ?u.4933} → {β : Type ?u.4932} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter f: α → βf l: Filter αl a: αa) (l': ?m.4969l') : IsMaxFilter: {α : Type ?u.4973} → {β : Type ?u.4972} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter f: α → βf (l: Filter αl ⊓ l': ?m.4969l') a: αa :=
h: IsMaxFilter f l ah.filter_mono: ∀ {α : Type ?u.5039} {β : Type ?u.5038} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α},
IsMaxFilter f l a → l' ≤ l → IsMaxFilter f l' afilter_mono inf_le_left: ∀ {α : Type ?u.5064} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ ainf_le_left
#align is_max_filter.filter_inf IsMaxFilter.filter_inf: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter f l a → ∀ (l' : Filter α), IsMaxFilter f (l ⊓ l') aIsMaxFilter.filter_inf

theorem IsExtrFilter.filter_inf: IsExtrFilter f l a → ∀ (l' : Filter α), IsExtrFilter f (l ⊓ l') aIsExtrFilter.filter_inf (h: IsExtrFilter f l ah : IsExtrFilter: {α : Type ?u.5204} → {β : Type ?u.5203} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsExtrFilter f: α → βf l: Filter αl a: αa) (l': ?m.5240l') : IsExtrFilter: {α : Type ?u.5244} → {β : Type ?u.5243} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsExtrFilter f: α → βf (l: Filter αl ⊓ l': ?m.5240l') a: αa :=
h: IsExtrFilter f l ah.filter_mono: ∀ {α : Type ?u.5310} {β : Type ?u.5309} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α},
IsExtrFilter f l a → l' ≤ l → IsExtrFilter f l' afilter_mono inf_le_left: ∀ {α : Type ?u.5335} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ ainf_le_left
#align is_extr_filter.filter_inf IsExtrFilter.filter_inf: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsExtrFilter f l a → ∀ (l' : Filter α), IsExtrFilter f (l ⊓ l') aIsExtrFilter.filter_inf

theorem IsMinOn.on_subset: IsMinOn f t a → s ⊆ t → IsMinOn f s aIsMinOn.on_subset (hf: IsMinOn f t ahf : IsMinOn: {α : Type ?u.5475} → {β : Type ?u.5474} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn f: α → βf t: Set αt a: αa) (h: s ⊆ th : s: Set αs ⊆ t: Set αt) : IsMinOn: {α : Type ?u.5533} → {β : Type ?u.5532} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn f: α → βf s: Set αs a: αa :=
hf: IsMinOn f t ahf.filter_mono: ∀ {α : Type ?u.5569} {β : Type ?u.5568} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α},
IsMinFilter f l a → l' ≤ l → IsMinFilter f l' afilter_mono <| principal_mono: ∀ {α : Type ?u.5595} {s t : Set α}, 𝓟 s ≤ 𝓟 t ↔ s ⊆ tprincipal_mono.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 h: s ⊆ th
#align is_min_on.on_subset IsMinOn.on_subset: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set α},
IsMinOn f t a → s ⊆ t → IsMinOn f s aIsMinOn.on_subset

theorem IsMaxOn.on_subset: IsMaxOn f t a → s ⊆ t → IsMaxOn f s aIsMaxOn.on_subset (hf: IsMaxOn f t ahf : IsMaxOn: {α : Type ?u.5662} → {β : Type ?u.5661} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn f: α → βf t: Set αt a: αa) (h: s ⊆ th : s: Set αs ⊆ t: Set αt) : IsMaxOn: {α : Type ?u.5720} → {β : Type ?u.5719} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn f: α → βf s: Set αs a: αa :=
hf: IsMaxOn f t ahf.filter_mono: ∀ {α : Type ?u.5756} {β : Type ?u.5755} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α},
IsMaxFilter f l a → l' ≤ l → IsMaxFilter f l' afilter_mono <| principal_mono: ∀ {α : Type ?u.5782} {s t : Set α}, 𝓟 s ≤ 𝓟 t ↔ s ⊆ tprincipal_mono.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 h: s ⊆ th
#align is_max_on.on_subset IsMaxOn.on_subset: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set α},
IsMaxOn f t a → s ⊆ t → IsMaxOn f s aIsMaxOn.on_subset

theorem IsExtrOn.on_subset: IsExtrOn f t a → s ⊆ t → IsExtrOn f s aIsExtrOn.on_subset (hf: IsExtrOn f t ahf : IsExtrOn: {α : Type ?u.5849} → {β : Type ?u.5848} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn f: α → βf t: Set αt a: αa) (h: s ⊆ th : s: Set αs ⊆ t: Set αt) : IsExtrOn: {α : Type ?u.5907} → {β : Type ?u.5906} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn f: α → βf s: Set αs a: αa :=
hf: IsExtrOn f t ahf.filter_mono: ∀ {α : Type ?u.5943} {β : Type ?u.5942} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α},
IsExtrFilter f l a → l' ≤ l → IsExtrFilter f l' afilter_mono <| principal_mono: ∀ {α : Type ?u.5969} {s t : Set α}, 𝓟 s ≤ 𝓟 t ↔ s ⊆ tprincipal_mono.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 h: s ⊆ th
#align is_extr_on.on_subset IsExtrOn.on_subset: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set α},
IsExtrOn f t a → s ⊆ t → IsExtrOn f s aIsExtrOn.on_subset

theorem IsMinOn.inter: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMinOn f s a → ∀ (t : Set α), IsMinOn f (s ∩ t) aIsMinOn.inter (hf: IsMinOn f s ahf : IsMinOn: {α : Type ?u.6036} → {β : Type ?u.6035} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn f: α → βf s: Set αs a: αa) (t: ?m.6073t) : IsMinOn: {α : Type ?u.6077} → {β : Type ?u.6076} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn f: α → βf (s: Set αs ∩ t: ?m.6073t) a: αa :=
hf: IsMinOn f s ahf.on_subset: ∀ {α : Type ?u.6130} {β : Type ?u.6129} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set α},
IsMinOn f t a → s ⊆ t → IsMinOn f s aon_subset (inter_subset_left: ∀ {α : Type ?u.6160} (s t : Set α), s ∩ t ⊆ sinter_subset_left s: Set αs t: Set αt)
#align is_min_on.inter IsMinOn.inter: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMinOn f s a → ∀ (t : Set α), IsMinOn f (s ∩ t) aIsMinOn.inter

theorem IsMaxOn.inter: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMaxOn f s a → ∀ (t : Set α), IsMaxOn f (s ∩ t) aIsMaxOn.inter (hf: IsMaxOn f s ahf : IsMaxOn: {α : Type ?u.6208} → {β : Type ?u.6207} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn f: α → βf s: Set αs a: αa) (t: ?m.6245t) : IsMaxOn: {α : Type ?u.6249} → {β : Type ?u.6248} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn f: α → βf (s: Set αs ∩ t: ?m.6245t) a: αa :=
hf: IsMaxOn f s ahf.on_subset: ∀ {α : Type ?u.6302} {β : Type ?u.6301} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set α},
IsMaxOn f t a → s ⊆ t → IsMaxOn f s aon_subset (inter_subset_left: ∀ {α : Type ?u.6332} (s t : Set α), s ∩ t ⊆ sinter_subset_left s: Set αs t: Set αt)
#align is_max_on.inter IsMaxOn.inter: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMaxOn f s a → ∀ (t : Set α), IsMaxOn f (s ∩ t) aIsMaxOn.inter

theorem IsExtrOn.inter: IsExtrOn f s a → ∀ (t : Set α), IsExtrOn f (s ∩ t) aIsExtrOn.inter (hf: IsExtrOn f s ahf : IsExtrOn: {α : Type ?u.6380} → {β : Type ?u.6379} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn f: α → βf s: Set αs a: αa) (t: ?m.6417t) : IsExtrOn: {α : Type ?u.6421} → {β : Type ?u.6420} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn f: α → βf (s: Set αs ∩ t: ?m.6417t) a: αa :=
hf: IsExtrOn f s ahf.on_subset: ∀ {α : Type ?u.6474} {β : Type ?u.6473} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set α},
IsExtrOn f t a → s ⊆ t → IsExtrOn f s aon_subset (inter_subset_left: ∀ {α : Type ?u.6500} (s t : Set α), s ∩ t ⊆ sinter_subset_left s: Set αs t: Set αt)
#align is_extr_on.inter IsExtrOn.inter: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsExtrOn f s a → ∀ (t : Set α), IsExtrOn f (s ∩ t) aIsExtrOn.inter

/-! ### Composition with (anti)monotone functions -/

theorem IsMinFilter.comp_mono: IsMinFilter f l a → ∀ {g : β → γ}, Monotone g → IsMinFilter (g ∘ f) l aIsMinFilter.comp_mono (hf: IsMinFilter f l ahf : IsMinFilter: {α : Type ?u.6548} → {β : Type ?u.6547} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter f: α → βf l: Filter αl a: αa) {g: β → γg : β: Type vβ → γ: Type wγ} (hg: Monotone ghg : Monotone: {α : Type ?u.6589} → {β : Type ?u.6588} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone g: β → γg) :
IsMinFilter: {α : Type ?u.6648} → {β : Type ?u.6647} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter (g: β → γg ∘ f: α → βf) l: Filter αl a: αa :=
mem_of_superset: ∀ {α : Type ?u.6698} {f : Filter α} {x y : Set α}, x ∈ f → x ⊆ y → y ∈ fmem_of_superset hf: IsMinFilter f l ahf fun _x: ?m.6712_x hx: ?m.6715hx => hg: Monotone ghg hx: ?m.6715hx
#align is_min_filter.comp_mono 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 aIsMinFilter.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 aIsMaxFilter.comp_mono (hf: IsMaxFilter f l ahf : IsMaxFilter: {α : Type ?u.6779} → {β : Type ?u.6778} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter f: α → βf l: Filter αl a: αa) {g: β → γg : β: Type vβ → γ: Type wγ} (hg: Monotone ghg : Monotone: {α : Type ?u.6820} → {β : Type ?u.6819} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone g: β → γg) :
IsMaxFilter: {α : Type ?u.6879} → {β : Type ?u.6878} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter (g: β → γg ∘ f: α → βf) l: Filter αl a: αa :=
mem_of_superset: ∀ {α : Type ?u.6929} {f : Filter α} {x y : Set α}, x ∈ f → x ⊆ y → y ∈ fmem_of_superset hf: IsMaxFilter f l ahf fun _x: ?m.6943_x hx: ?m.6946hx => hg: Monotone ghg hx: ?m.6946hx
#align is_max_filter.comp_mono 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 aIsMaxFilter.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 aIsExtrFilter.comp_mono (hf: IsExtrFilter f l ahf : IsExtrFilter: {α : Type ?u.7010} → {β : Type ?u.7009} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsExtrFilter f: α → βf l: Filter αl a: αa) {g: β → γg : β: Type vβ → γ: Type wγ} (hg: Monotone ghg : Monotone: {α : Type ?u.7051} → {β : Type ?u.7050} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone g: β → γg) :
IsExtrFilter: {α : Type ?u.7110} → {β : Type ?u.7109} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsExtrFilter (g: β → γg ∘ f: α → βf) l: Filter αl a: αa :=
hf: IsExtrFilter f l ahf.elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → celim (fun hf: ?m.7172hf => (hf: ?m.7172hf.comp_mono: ∀ {α : Type ?u.7176} {β : Type ?u.7175} {γ : Type ?u.7174} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β}
{l : Filter α} {a : α}, IsMinFilter f l a → ∀ {g : β → γ}, Monotone g → IsMinFilter (g ∘ f) l acomp_mono hg: Monotone ghg).isExtr: ∀ {α : Type ?u.7219} {β : Type ?u.7218} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter f l a → IsExtrFilter f l aisExtr) fun hf: ?m.7251hf => (hf: ?m.7251hf.comp_mono: ∀ {α : Type ?u.7255} {β : Type ?u.7254} {γ : Type ?u.7253} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β}
{l : Filter α} {a : α}, IsMaxFilter f l a → ∀ {g : β → γ}, Monotone g → IsMaxFilter (g ∘ f) l acomp_mono hg: Monotone ghg).isExtr: ∀ {α : Type ?u.7292} {β : Type ?u.7291} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter f l a → IsExtrFilter f l aisExtr
#align is_extr_filter.comp_mono 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 aIsExtrFilter.comp_mono

theorem IsMinFilter.comp_antitone: IsMinFilter f l a → ∀ {g : β → γ}, Antitone g → IsMaxFilter (g ∘ f) l aIsMinFilter.comp_antitone (hf: IsMinFilter f l ahf : IsMinFilter: {α : Type ?u.7365} → {β : Type ?u.7364} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter f: α → βf l: Filter αl a: αa) {g: β → γg : β: Type vβ → γ: Type wγ} (hg: Antitone ghg : Antitone: {α : Type ?u.7406} → {β : Type ?u.7405} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone g: β → γg) :
IsMaxFilter: {α : Type ?u.7465} → {β : Type ?u.7464} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter (g: β → γg ∘ f: α → βf) l: Filter αl a: αa :=
hf: IsMinFilter f l ahf.dual: ∀ {α : Type ?u.7516} {β : Type ?u.7515} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter f l a → IsMaxFilter (↑toDual ∘ f) l adual.comp_mono: ∀ {α : Type ?u.7533} {β : Type ?u.7532} {γ : Type ?u.7531} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β}
{l : Filter α} {a : α}, IsMaxFilter f l a → ∀ {g : β → γ}, Monotone g → IsMaxFilter (g ∘ f) l acomp_mono fun _: ?m.7609_ _: ?m.7612_ h: ?m.7615h => hg: Antitone ghg h: ?m.7615h
#align is_min_filter.comp_antitone 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 aIsMinFilter.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 aIsMaxFilter.comp_antitone (hf: IsMaxFilter f l ahf : IsMaxFilter: {α : Type ?u.7682} → {β : Type ?u.7681} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter f: α → βf l: Filter αl a: αa) {g: β → γg : β: Type vβ → γ: Type wγ} (hg: Antitone ghg : Antitone: {α : Type ?u.7723} → {β : Type ?u.7722} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone g: β → γg) :
IsMinFilter: {α : Type ?u.7782} → {β : Type ?u.7781} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter (g: β → γg ∘ f: α → βf) l: Filter αl a: αa :=
hf: IsMaxFilter f l ahf.dual: ∀ {α : Type ?u.7833} {β : Type ?u.7832} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter f l a → IsMinFilter (↑toDual ∘ f) l adual.comp_mono: ∀ {α : Type ?u.7850} {β : Type ?u.7849} {γ : Type ?u.7848} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β}
{l : Filter α} {a : α}, IsMinFilter f l a → ∀ {g : β → γ}, Monotone g → IsMinFilter (g ∘ f) l acomp_mono fun _: ?m.7926_ _: ?m.7929_ h: ?m.7932h => hg: Antitone ghg h: ?m.7932h
#align is_max_filter.comp_antitone 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 aIsMaxFilter.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 aIsExtrFilter.comp_antitone (hf: IsExtrFilter f l ahf : IsExtrFilter: {α : Type ?u.7999} → {β : Type ?u.7998} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsExtrFilter f: α → βf l: Filter αl a: αa) {g: β → γg : β: Type vβ → γ: Type wγ} (hg: Antitone ghg : Antitone: {α : Type ?u.8040} → {β : Type ?u.8039} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone g: β → γg) :
IsExtrFilter: {α : Type ?u.8099} → {β : Type ?u.8098} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsExtrFilter (g: β → γg ∘ f: α → βf) l: Filter αl a: αa :=
hf: IsExtrFilter f l ahf.dual: ∀ {α : Type ?u.8150} {β : Type ?u.8149} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsExtrFilter f l a → IsExtrFilter (↑toDual ∘ f) l adual.comp_mono: ∀ {α : Type ?u.8167} {β : Type ?u.8166} {γ : Type ?u.8165} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β}
{l : Filter α} {a : α}, IsExtrFilter f l a → ∀ {g : β → γ}, Monotone g → IsExtrFilter (g ∘ f) l acomp_mono fun _: ?m.8236_ _: ?m.8239_ h: ?m.8242h => hg: Antitone ghg h: ?m.8242h
#align is_extr_filter.comp_antitone 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 aIsExtrFilter.comp_antitone

theorem IsMinOn.comp_mono: ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α} {a : α},
IsMinOn f s a → ∀ {g : β → γ}, Monotone g → IsMinOn (g ∘ f) s aIsMinOn.comp_mono (hf: IsMinOn f s ahf : IsMinOn: {α : Type ?u.8309} → {β : Type ?u.8308} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn f: α → βf s: Set αs a: αa) {g: β → γg : β: Type vβ → γ: Type wγ} (hg: Monotone ghg : Monotone: {α : Type ?u.8351} → {β : Type ?u.8350} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone g: β → γg) :
IsMinOn: {α : Type ?u.8410} → {β : Type ?u.8409} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn (g: β → γg ∘ f: α → βf) s: Set αs a: αa :=
IsMinFilter.comp_mono: ∀ {α : Type ?u.8463} {β : Type ?u.8462} {γ : Type ?u.8461} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β}
{l : Filter α} {a : α}, IsMinFilter f l a → ∀ {g : β → γ}, Monotone g → IsMinFilter (g ∘ f) l aIsMinFilter.comp_mono hf: IsMinOn f s ahf hg: Monotone ghg
#align is_min_on.comp_mono IsMinOn.comp_mono: ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α} {a : α},
IsMinOn f s a → ∀ {g : β → γ}, Monotone g → IsMinOn (g ∘ f) s aIsMinOn.comp_mono

theorem IsMaxOn.comp_mono: ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α} {a : α},
IsMaxOn f s a → ∀ {g : β → γ}, Monotone g → IsMaxOn (g ∘ f) s aIsMaxOn.comp_mono (hf: IsMaxOn f s ahf : IsMaxOn: {α : Type ?u.8574} → {β : Type ?u.8573} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn f: α → βf s: Set αs a: αa) {g: β → γg : β: Type vβ → γ: Type wγ} (hg: Monotone ghg : Monotone: {α : Type ?u.8616} → {β : Type ?u.8615} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone g: β → γg) :
IsMaxOn: {α : Type ?u.8675} → {β : Type ?u.8674} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn (g: β → γg ∘ f: α → βf) s: Set αs a: αa :=
IsMaxFilter.comp_mono: ∀ {α : Type ?u.8728} {β : Type ?u.8727} {γ : Type ?u.8726} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β}
{l : Filter α} {a : α}, IsMaxFilter f l a → ∀ {g : β → γ}, Monotone g → IsMaxFilter (g ∘ f) l aIsMaxFilter.comp_mono hf: IsMaxOn f s ahf hg: Monotone ghg
#align is_max_on.comp_mono IsMaxOn.comp_mono: ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α} {a : α},
IsMaxOn f s a → ∀ {g : β → γ}, Monotone g → IsMaxOn (g ∘ f) s aIsMaxOn.comp_mono

theorem IsExtrOn.comp_mono: ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α} {a : α},
IsExtrOn f s a → ∀ {g : β → γ}, Monotone g → IsExtrOn (g ∘ f) s aIsExtrOn.comp_mono (hf: IsExtrOn f s ahf : IsExtrOn: {α : Type ?u.8839} → {β : Type ?u.8838} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn f: α → βf s: Set αs a: αa) {g: β → γg : β: Type vβ → γ: Type wγ} (hg: Monotone ghg : Monotone: {α : Type ?u.8881} → {β : Type ?u.8880} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone g: β → γg) :
IsExtrOn: {α : Type ?u.8940} → {β : Type ?u.8939} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn (g: β → γg ∘ f: α → βf) s: Set αs a: αa :=
IsExtrFilter.comp_mono: ∀ {α : Type ?u.8993} {β : Type ?u.8992} {γ : Type ?u.8991} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β}
{l : Filter α} {a : α}, IsExtrFilter f l a → ∀ {g : β → γ}, Monotone g → IsExtrFilter (g ∘ f) l aIsExtrFilter.comp_mono hf: IsExtrOn f s ahf hg: Monotone ghg
#align is_extr_on.comp_mono IsExtrOn.comp_mono: ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α} {a : α},
IsExtrOn f s a → ∀ {g : β → γ}, Monotone g → IsExtrOn (g ∘ f) s aIsExtrOn.comp_mono

theorem IsMinOn.comp_antitone: ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α} {a : α},
IsMinOn f s a → ∀ {g : β → γ}, Antitone g → IsMaxOn (g ∘ f) s aIsMinOn.comp_antitone (hf: IsMinOn f s ahf : IsMinOn: {α : Type ?u.9102} → {β : Type ?u.9101} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn f: α → βf s: Set αs a: αa) {g: β → γg : β: Type vβ → γ: Type wγ} (hg: Antitone ghg : Antitone: {α : Type ?u.9144} → {β : Type ?u.9143} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone g: β → γg) :
IsMaxOn: {α : Type ?u.9203} → {β : Type ?u.9202} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn (g: β → γg ∘ f: α → βf) s: Set αs a: αa :=
IsMinFilter.comp_antitone: ∀ {α : Type ?u.9256} {β : Type ?u.9255} {γ : Type ?u.9254} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β}
{l : Filter α} {a : α}, IsMinFilter f l a → ∀ {g : β → γ}, Antitone g → IsMaxFilter (g ∘ f) l aIsMinFilter.comp_antitone hf: IsMinOn f s ahf hg: Antitone ghg
#align is_min_on.comp_antitone IsMinOn.comp_antitone: ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α} {a : α},
IsMinOn f s a → ∀ {g : β → γ}, Antitone g → IsMaxOn (g ∘ f) s aIsMinOn.comp_antitone

theorem IsMaxOn.comp_antitone: IsMaxOn f s a → ∀ {g : β → γ}, Antitone g → IsMinOn (g ∘ f) s aIsMaxOn.comp_antitone (hf: IsMaxOn f s ahf : IsMaxOn: {α : Type ?u.9367} → {β : Type ?u.9366} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn f: α → βf s: Set αs a: αa) {g: β → γg : β: Type vβ → γ: Type wγ} (hg: Antitone ghg : Antitone: {α : Type ?u.9409} → {β : Type ?u.9408} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone g: β → γg) :
IsMinOn: {α : Type ?u.9468} → {β : Type ?u.9467} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn (g: β → γg ∘ f: α → βf) s: Set αs a: αa :=
IsMaxFilter.comp_antitone: ∀ {α : Type ?u.9521} {β : Type ?u.9520} {γ : Type ?u.9519} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β}
{l : Filter α} {a : α}, IsMaxFilter f l a → ∀ {g : β → γ}, Antitone g → IsMinFilter (g ∘ f) l aIsMaxFilter.comp_antitone hf: IsMaxOn f s ahf hg: Antitone ghg
#align is_max_on.comp_antitone IsMaxOn.comp_antitone: ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α} {a : α},
IsMaxOn f s a → ∀ {g : β → γ}, Antitone g → IsMinOn (g ∘ f) s aIsMaxOn.comp_antitone

theorem IsExtrOn.comp_antitone: IsExtrOn f s a → ∀ {g : β → γ}, Antitone g → IsExtrOn (g ∘ f) s aIsExtrOn.comp_antitone (hf: IsExtrOn f s ahf : IsExtrOn: {α : Type ?u.9632} → {β : Type ?u.9631} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn f: α → βf s: Set αs a: αa) {g: β → γg : β: Type vβ → γ: Type wγ} (hg: Antitone ghg : Antitone: {α : Type ?u.9674} → {β : Type ?u.9673} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone g: β → γg) :
IsExtrOn: {α : Type ?u.9733} → {β : Type ?u.9732} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn (g: β → γg ∘ f: α → βf) s: Set αs a: αa :=
IsExtrFilter.comp_antitone: ∀ {α : Type ?u.9786} {β : Type ?u.9785} {γ : Type ?u.9784} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β}
{l : Filter α} {a : α}, IsExtrFilter f l a → ∀ {g : β → γ}, Antitone g → IsExtrFilter (g ∘ f) l aIsExtrFilter.comp_antitone hf: IsExtrOn f s ahf hg: Antitone ghg
#align is_extr_on.comp_antitone IsExtrOn.comp_antitone: ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α} {a : α},
IsExtrOn f s a → ∀ {g : β → γ}, Antitone g → IsExtrOn (g ∘ f) s aIsExtrOn.comp_antitone

theorem IsMinFilter.bicomp_mono: ∀ [inst : 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 aIsMinFilter.bicomp_mono [Preorder: Type ?u.9894 → Type ?u.9894Preorder δ: Type xδ] {op: β → γ → δop : β: Type vβ → γ: Type wγ → δ: Type xδ}
(hop: ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op ophop : ((· ≤ ·): β → β → Prop(· ≤ ·) ⇒ (· ≤ ·): γ → γ → Prop(· ≤ ·) ⇒ (· ≤ ·): δ → δ → Prop(· ≤ ·)) op: β → γ → δop op: β → γ → δop) (hf: IsMinFilter f l ahf : IsMinFilter: {α : Type ?u.10153} → {β : Type ?u.10152} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter f: α → βf l: Filter αl a: αa) {g: α → γg : α: Type uα → γ: Type wγ}
(hg: IsMinFilter g l ahg : IsMinFilter: {α : Type ?u.10194} → {β : Type ?u.10193} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter g: α → γg l: Filter αl a: αa) : IsMinFilter: {α : Type ?u.10230} → {β : Type ?u.10229} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter (fun x: ?m.10257x => op: β → γ → δop (f: α → βf x: ?m.10257x) (g: α → γg x: ?m.10257x)) l: Filter αl a: αa :=
mem_of_superset: ∀ {α : Type ?u.10314} {f : Filter α} {x y : Set α}, x ∈ f → x ⊆ y → y ∈ fmem_of_superset (inter_mem: ∀ {α : Type ?u.10327} {f : Filter α} {s t : Set α}, s ∈ f → t ∈ f → s ∩ t ∈ finter_mem hf: IsMinFilter f l ahf hg: IsMinFilter g l ahg) fun _x: ?m.10333_x ⟨hfx: _x ∈ { x | (fun x => f a ≤ f x) x }hfx, hgx: _x ∈ { x | (fun x => g a ≤ g x) x }hgx⟩ => hop: ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op ophop hfx: _x ∈ { x | (fun x => f a ≤ f x) x }hfx hgx: _x ∈ { x | (fun x => g a ≤ g x) x }hgx
#align is_min_filter.bicomp_mono 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 aIsMinFilter.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 aIsMaxFilter.bicomp_mono [Preorder: Type ?u.10554 → Type ?u.10554Preorder δ: Type xδ] {op: β → γ → δop : β: Type vβ → γ: Type wγ → δ: Type xδ}
(hop: ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op ophop : ((· ≤ ·): β → β → Prop(· ≤ ·) ⇒ (· ≤ ·): γ → γ → Prop(· ≤ ·) ⇒ (· ≤ ·): δ → δ → Prop(· ≤ ·)) op: β → γ → δop op: β → γ → δop) (hf: IsMaxFilter f l ahf : IsMaxFilter: {α : Type ?u.10813} → {β : Type ?u.10812} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter f: α → βf l: Filter αl a: αa) {g: α → γg : α: Type uα → γ: Type wγ}
(hg: IsMaxFilter g l ahg : IsMaxFilter: {α : Type ?u.10854} → {β : Type ?u.10853} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter g: α → γg l: Filter αl a: αa) : IsMaxFilter: {α : Type ?u.10890} → {β : Type ?u.10889} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter (fun x: ?m.10917x => op: β → γ → δop (f: α → βf x: ?m.10917x) (g: α → γg x: ?m.10917x)) l: Filter αl a: αa :=
mem_of_superset: ∀ {α : Type ?u.10974} {f : Filter α} {x y : Set α}, x ∈ f → x ⊆ y → y ∈ fmem_of_superset (inter_mem: ∀ {α : Type ?u.10987} {f : Filter α} {s t : Set α}, s ∈ f → t ∈ f → s ∩ t ∈ finter_mem hf: IsMaxFilter f l ahf hg: IsMaxFilter g l ahg) fun _x: ?m.10993_x ⟨hfx: _x ∈ { x | (fun x => f x ≤ f a) x }hfx, hgx: _x ∈ { x | (fun x => g x ≤ g a) x }hgx⟩ => hop: ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op ophop hfx: _x ∈ { x | (fun x => f x ≤ f a) x }hfx hgx: _x ∈ { x | (fun x => g x ≤ g a) x }hgx
#align is_max_filter.bicomp_mono 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 aIsMaxFilter.bicomp_mono

-- No `Extr` version because we need `hf` and `hg` to be of the same kind
theorem IsMinOn.bicomp_mono: ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α}
{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 →
IsMinOn f s a → ∀ {g : α → γ}, IsMinOn g s a → IsMinOn (fun x => op (f x) (g x)) s aIsMinOn.bicomp_mono [Preorder: Type ?u.11214 → Type ?u.11214Preorder δ: Type xδ] {op: β → γ → δop : β: Type vβ → γ: Type wγ → δ: Type xδ}
(hop: ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op ophop : ((· ≤ ·): β → β → Prop(· ≤ ·) ⇒ (· ≤ ·): γ → γ → Prop(· ≤ ·) ⇒ (· ≤ ·): δ → δ → Prop(· ≤ ·)) op: β → γ → δop op: β → γ → δop) (hf: IsMinOn f s ahf : IsMinOn: {α : Type ?u.11473} → {β : Type ?u.11472} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn f: α → βf s: Set αs a: αa) {g: α → γg : α: Type uα → γ: Type wγ}
(hg: IsMinOn g s ahg : IsMinOn: {α : Type ?u.11515} → {β : Type ?u.11514} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn g: α → γg s: Set αs a: αa) : IsMinOn: {α : Type ?u.11552} → {β : Type ?u.11551} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn (fun x: ?m.11579x => op: β → γ → δop (f: α → βf x: ?m.11579x) (g: α → γg x: ?m.11579x)) s: Set αs a: αa :=
IsMinFilter.bicomp_mono: ∀ {α : Type ?u.11640} {β : Type ?u.11639} {γ : Type ?u.11638} {δ : Type ?u.11637} [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 aIsMinFilter.bicomp_mono hop: ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op ophop hf: IsMinOn f s ahf hg: IsMinOn g s ahg
#align is_min_on.bicomp_mono IsMinOn.bicomp_mono: ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α}
{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 →
IsMinOn f s a → ∀ {g : α → γ}, IsMinOn g s a → IsMinOn (fun x => op (f x) (g x)) s aIsMinOn.bicomp_mono

theorem IsMaxOn.bicomp_mono: ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α}
{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 →
IsMaxOn f s a → ∀ {g : α → γ}, IsMaxOn g s a → IsMaxOn (fun x => op (f x) (g x)) s aIsMaxOn.bicomp_mono [Preorder: Type ?u.11814 → Type ?u.11814Preorder δ: Type xδ] {op: β → γ → δop : β: Type vβ → γ: Type wγ → δ: Type xδ}
(hop: ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op ophop : ((· ≤ ·): β → β → Prop(· ≤ ·) ⇒ (· ≤ ·): γ → γ → Prop(· ≤ ·) ⇒ (· ≤ ·): δ → δ → Prop(· ≤ ·)) op: β → γ → δop op: β → γ → δop) (hf: IsMaxOn f s ahf : IsMaxOn: {α : Type ?u.12073} → {β : Type ?u.12072} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn f: α → βf s: Set αs a: αa) {g: α → γg : α: Type uα → γ: Type wγ}
(hg: IsMaxOn g s ahg : IsMaxOn: {α : Type ?u.12115} → {β : Type ?u.12114} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn g: α → γg s: Set αs a: αa) : IsMaxOn: {α : Type ?u.12152} → {β : Type ?u.12151} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn (fun x: ?m.12179x => op: β → γ → δop (f: α → βf x: ?m.12179x) (g: α → γg x: ?m.12179x)) s: Set αs a: αa :=
IsMaxFilter.bicomp_mono: ∀ {α : Type ?u.12240} {β : Type ?u.12239} {γ : Type ?u.12238} {δ : Type ?u.12237} [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 aIsMaxFilter.bicomp_mono hop: ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op ophop hf: IsMaxOn f s ahf hg: IsMaxOn g s ahg
#align is_max_on.bicomp_mono IsMaxOn.bicomp_mono: ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α}
{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 →
IsMaxOn f s a → ∀ {g : α → γ}, IsMaxOn g s a → IsMaxOn (fun x => op (f x) (g x)) s aIsMaxOn.bicomp_mono

/-! ### Composition with `Tendsto` -/

theorem IsMinFilter.comp_tendsto: ∀ {g : δ → α} {l' : Filter δ} {b : δ}, IsMinFilter f l (g b) → Tendsto g l' l → IsMinFilter (f ∘ g) l' bIsMinFilter.comp_tendsto {g: δ → αg : δ: Type xδ → α: Type uα} {l': Filter δl' : Filter: Type ?u.12418 → Type ?u.12418Filter δ: Type xδ} {b: δb : δ: Type xδ} (hf: IsMinFilter f l (g b)hf : IsMinFilter: {α : Type ?u.12424} → {β : Type ?u.12423} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter f: α → βf l: Filter αl (g: δ → αg b: δb))
(hg: Tendsto g l' lhg : Tendsto: {α : Type ?u.12461} → {β : Type ?u.12460} → (α → β) → Filter α → Filter β → PropTendsto g: δ → αg l': Filter δl' l: Filter αl) : IsMinFilter: {α : Type ?u.12471} → {β : Type ?u.12470} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMinFilter (f: α → βf ∘ g: δ → αg) l': Filter δl' b: δb :=
hg: Tendsto g l' lhg hf: IsMinFilter f l (g b)hf
#align is_min_filter.comp_tendsto IsMinFilter.comp_tendsto: ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {l : Filter α} {g : δ → α} {l' : Filter δ}
{b : δ}, IsMinFilter f l (g b) → Tendsto g l' l → IsMinFilter (f ∘ g) l' bIsMinFilter.comp_tendsto

theorem IsMaxFilter.comp_tendsto: ∀ {g : δ → α} {l' : Filter δ} {b : δ}, IsMaxFilter f l (g b) → Tendsto g l' l → IsMaxFilter (f ∘ g) l' bIsMaxFilter.comp_tendsto {g: δ → αg : δ: Type xδ → α: Type uα} {l': Filter δl' : Filter: Type ?u.12627 → Type ?u.12627Filter δ: Type xδ} {b: δb : δ: Type xδ} (hf: IsMaxFilter f l (g b)hf : IsMaxFilter: {α : Type ?u.12633} → {β : Type ?u.12632} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter f: α → βf l: Filter αl (g: δ → αg b: δb))
(hg: Tendsto g l' lhg : Tendsto: {α : Type ?u.12670} → {β : Type ?u.12669} → (α → β) → Filter α → Filter β → PropTendsto g: δ → αg l': Filter δl' l: Filter αl) : IsMaxFilter: {α : Type ?u.12680} → {β : Type ?u.12679} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsMaxFilter (f: α → βf ∘ g: δ → αg) l': Filter δl' b: δb :=
hg: Tendsto g l' lhg hf: IsMaxFilter f l (g b)hf
#align is_max_filter.comp_tendsto IsMaxFilter.comp_tendsto: ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {l : Filter α} {g : δ → α} {l' : Filter δ}
{b : δ}, IsMaxFilter f l (g b) → Tendsto g l' l → IsMaxFilter (f ∘ g) l' bIsMaxFilter.comp_tendsto

theorem IsExtrFilter.comp_tendsto: ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {l : Filter α} {g : δ → α} {l' : Filter δ}
{b : δ}, IsExtrFilter f l (g b) → Tendsto g l' l → IsExtrFilter (f ∘ g) l' bIsExtrFilter.comp_tendsto {g: δ → αg : δ: Type xδ → α: Type uα} {l': Filter δl' : Filter: Type ?u.12836 → Type ?u.12836Filter δ: Type xδ} {b: δb : δ: Type xδ} (hf: IsExtrFilter f l (g b)hf : IsExtrFilter: {α : Type ?u.12842} → {β : Type ?u.12841} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsExtrFilter f: α → βf l: Filter αl (g: δ → αg b: δb))
(hg: Tendsto g l' lhg : Tendsto: {α : Type ?u.12879} → {β : Type ?u.12878} → (α → β) → Filter α → Filter β → PropTendsto g: δ → αg l': Filter δl' l: Filter αl) : IsExtrFilter: {α : Type ?u.12889} → {β : Type ?u.12888} → [inst : Preorder β] → (α → β) → Filter α → α → PropIsExtrFilter (f: α → βf ∘ g: δ → αg) l': Filter δl' b: δb :=
hf: IsExtrFilter f l (g b)hf.elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → celim (fun hf: ?m.12955hf => (hf: ?m.12955hf.comp_tendsto: ∀ {α : Type ?u.12959} {β : Type ?u.12958} {δ : Type ?u.12957} [inst : Preorder β] {f : α → β} {l : Filter α} {g : δ → α}
{l' : Filter δ} {b : δ}, IsMinFilter f l (g b) → Tendsto g l' l → IsMinFilter (f ∘ g) l' bcomp_tendsto hg: Tendsto g l' lhg).isExtr: ∀ {α : Type ?u.12996} {β : Type ?u.12995} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMinFilter f l a → IsExtrFilter f l aisExtr) fun hf: ?m.13028hf => (hf: ?m.13028hf.comp_tendsto: ∀ {α : Type ?u.13032} {β : Type ?u.13031} {δ : Type ?u.13030} [inst : Preorder β] {f : α → β} {l : Filter α} {g : δ → α}
{l' : Filter δ} {b : δ}, IsMaxFilter f l (g b) → Tendsto g l' l → IsMaxFilter (f ∘ g) l' bcomp_tendsto hg: Tendsto g l' lhg).isExtr: ∀ {α : Type ?u.13063} {β : Type ?u.13062} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
IsMaxFilter f l a → IsExtrFilter f l aisExtr
#align is_extr_filter.comp_tendsto IsExtrFilter.comp_tendsto: ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {l : Filter α} {g : δ → α} {l' : Filter δ}
{b : δ}, IsExtrFilter f l (g b) → Tendsto g l' l → IsExtrFilter (f ∘ g) l' bIsExtrFilter.comp_tendsto

theorem IsMinOn.on_preimage: ∀ (g : δ → α) {b : δ}, IsMinOn f s (g b) → IsMinOn (f ∘ g) (g ⁻¹' s) bIsMinOn.on_preimage (g: δ → αg : δ: Type xδ → α: Type uα) {b: δb : δ: Type xδ} (hf: IsMinOn f s (g b)hf : IsMinOn: {α : Type ?u.13142} → {β : Type ?u.13141} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn f: α → βf s: Set αs (g: δ → αg b: δb)) :
IsMinOn: {α : Type ?u.13180} → {β : Type ?u.13179} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn (f: α → βf ∘ g: δ → αg) (g: δ → αg ⁻¹' s: Set αs) b: δb :=
hf: IsMinOn f s (g b)hf.comp_tendsto: ∀ {α : Type ?u.13243} {β : Type ?u.13242} {δ : Type ?u.13241} [inst : Preorder β] {f : α → β} {l : Filter α} {g : δ → α}
{l' : Filter δ} {b : δ}, IsMinFilter f l (g b) → Tendsto g l' l → IsMinFilter (f ∘ g) l' bcomp_tendsto (tendsto_principal_principal: ∀ {α : Type ?u.13283} {β : Type ?u.13282} {f : α → β} {s : Set α} {t : Set β},
Tendsto f (𝓟 s) (𝓟 t) ↔ ∀ (a : α), a ∈ s → f a ∈ ttendsto_principal_principal.mpr: ∀ {a b : Prop}, (a ↔ b) → b → ampr <| Subset.refl: ∀ {α : Type ?u.13312} (a : Set α), a ⊆ aSubset.refl _: Set ?m.13313_)
#align is_min_on.on_preimage IsMinOn.on_preimage: ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {s : Set α} (g : δ → α) {b : δ},
IsMinOn f s (g b) → IsMinOn (f ∘ g) (g ⁻¹' s) bIsMinOn.on_preimage

theorem IsMaxOn.on_preimage: ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {s : Set α} (g : δ → α) {b : δ},
IsMaxOn f s (g b) → IsMaxOn (f ∘ g) (g ⁻¹' s) bIsMaxOn.on_preimage (g: δ → αg : δ: Type xδ → α: Type uα) {b: δb : δ: Type xδ} (hf: IsMaxOn f s (g b)hf : IsMaxOn: {α : Type ?u.13385} → {β : Type ?u.13384} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn f: α → βf s: Set αs (g: δ → αg b: δb)) :
IsMaxOn: {α : Type ?u.13423} → {β : Type ?u.13422} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn (f: α → βf ∘ g: δ → αg) (g: δ → αg ⁻¹' s: Set αs) b: δb :=
hf: IsMaxOn f s (g b)hf.comp_tendsto: ∀ {α : Type ?u.13486} {β : Type ?u.13485} {δ : Type ?u.13484} [inst : Preorder β] {f : α → β} {l : Filter α} {g : δ → α}
{l' : Filter δ} {b : δ}, IsMaxFilter f l (g b) → Tendsto g l' l → IsMaxFilter (f ∘ g) l' bcomp_tendsto (tendsto_principal_principal: ∀ {α : Type ?u.13526} {β : Type ?u.13525} {f : α → β} {s : Set α} {t : Set β},
Tendsto f (𝓟 s) (𝓟 t) ↔ ∀ (a : α), a ∈ s → f a ∈ ttendsto_principal_principal.mpr: ∀ {a b : Prop}, (a ↔ b) → b → ampr <| Subset.refl: ∀ {α : Type ?u.13555} (a : Set α), a ⊆ aSubset.refl _: Set ?m.13556_)
#align is_max_on.on_preimage IsMaxOn.on_preimage: ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {s : Set α} (g : δ → α) {b : δ},
IsMaxOn f s (g b) → IsMaxOn (f ∘ g) (g ⁻¹' s) bIsMaxOn.on_preimage

theorem IsExtrOn.on_preimage: ∀ (g : δ → α) {b : δ}, IsExtrOn f s (g b) → IsExtrOn (f ∘ g) (g ⁻¹' s) bIsExtrOn.on_preimage (g: δ → αg : δ: Type xδ → α: Type uα) {b: δb : δ: Type xδ} (hf: IsExtrOn f s (g b)hf : IsExtrOn: {α : Type ?u.13628} → {β : Type ?u.13627} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn f: α → βf s: Set αs (g: δ → αg b: δb)) :
IsExtrOn: {α : Type ?u.13666} → {β : Type ?u.13665} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn (f: α → βf ∘ g: δ → αg) (g: δ → αg ⁻¹' s: Set αs) b: δb :=
hf: IsExtrOn f s (g b)hf.elim: ∀ {α : Type ?u.13728} {β : Type ?u.13727} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {p : Prop},
IsExtrOn f s a → (IsMinOn f s a → p) → (IsMaxOn f s a → p) → pelim (fun hf: ?m.13756hf => (hf: ?m.13756hf.on_preimage: ∀ {α : Type ?u.13760} {β : Type ?u.13759} {δ : Type ?u.13758} [inst : Preorder β] {f : α → β} {s : Set α} (g : δ → α)
{b : δ}, IsMinOn f s (g b) → IsMinOn (f ∘ g) (g ⁻¹' s) bon_preimage g: δ → αg).isExtr: ∀ {α : Type ?u.13793} {β : Type ?u.13792} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMinOn f s a → IsExtrOn f s aisExtr) fun hf: ?m.13827hf => (hf: ?m.13827hf.on_preimage: ∀ {α : Type ?u.13831} {β : Type ?u.13830} {δ : Type ?u.13829} [inst : Preorder β] {f : α → β} {s : Set α} (g : δ → α)
{b : δ}, IsMaxOn f s (g b) → IsMaxOn (f ∘ g) (g ⁻¹' s) bon_preimage g: δ → αg).isExtr: ∀ {α : Type ?u.13863} {β : Type ?u.13862} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMaxOn f s a → IsExtrOn f s aisExtr
#align is_extr_on.on_preimage IsExtrOn.on_preimage: ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {s : Set α} (g : δ → α) {b : δ},
IsExtrOn f s (g b) → IsExtrOn (f ∘ g) (g ⁻¹' s) bIsExtrOn.on_preimage

theorem IsMinOn.comp_mapsTo: ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set δ} {g : δ → α}
{b : δ}, IsMinOn f s a → MapsTo g t s → g b = a → IsMinOn (f ∘ g) t bIsMinOn.comp_mapsTo {t: Set δt : Set: Type ?u.13934 → Type ?u.13934Set δ: Type xδ} {g: δ → αg : δ: Type xδ → α: Type uα} {b: δb : δ: Type xδ} (hf: IsMinOn f s ahf : IsMinOn: {α : Type ?u.13944} → {β : Type ?u.13943} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn f: α → βf s: Set αs a: αa) (hg: MapsTo g t shg : MapsTo: {α : Type ?u.13982} → {β : Type ?u.13981} → (α → β) → Set α → Set β → PropMapsTo g: δ → αg t: Set δt s: Set αs)
(ha: g b = aha : g: δ → αg b: δb = a: αa) : IsMinOn: {α : Type ?u.13998} → {β : Type ?u.13997} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMinOn (f: α → βf ∘ g: δ → αg) t: Set δt b: δb := fun y: ?m.14056y hy: ?m.14059hy => byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wδ: Type xinst✝¹: Preorder βinst✝: Preorder γf: α → βs: Set αl: Filter αa: αt✝: Set αl': Filter αt: Set δg: δ → αb: δhf: IsMinOn f s ahg: MapsTo g t sha: g b = ay: δhy: y ∈ ty ∈ { x | (fun x => (f ∘ g) b ≤ (f ∘ g) x) x }simpa only [ha: g b = aha, (· ∘ ·)] using hf: IsMinOn f s ahf (hg: MapsTo g t shg hy: y ∈ thy)Goals accomplished! 🐙
#align is_min_on.comp_maps_to IsMinOn.comp_mapsTo: ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set δ} {g : δ → α}
{b : δ}, IsMinOn f s a → MapsTo g t s → g b = a → IsMinOn (f ∘ g) t bIsMinOn.comp_mapsTo

theorem IsMaxOn.comp_mapsTo: ∀ {t : Set δ} {g : δ → α} {b : δ}, IsMaxOn f s a → MapsTo g t s → g b = a → IsMaxOn (f ∘ g) t bIsMaxOn.comp_mapsTo {t: Set δt : Set: Type ?u.14290 → Type ?u.14290Set δ: Type xδ} {g: δ → αg : δ: Type xδ → α: Type uα} {b: δb : δ: Type xδ} (hf: IsMaxOn f s ahf : IsMaxOn: {α : Type ?u.14300} → {β : Type ?u.14299} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn f: α → βf s: Set αs a: αa) (hg: MapsTo g t shg : MapsTo: {α : Type ?u.14338} → {β : Type ?u.14337} → (α → β) → Set α → Set β → PropMapsTo g: δ → αg t: Set δt s: Set αs)
(ha: g b = aha : g: δ → αg b: δb = a: αa) : IsMaxOn: {α : Type ?u.14354} → {β : Type ?u.14353} → [inst : Preorder β] → (α → β) → Set α → α → PropIsMaxOn (f: α → βf ∘ g: δ → αg) t: Set δt b: δb :=
hf: IsMaxOn f s ahf.dual: ∀ {α : Type ?u.14412} {β : Type ?u.14411} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
IsMaxOn f s a → IsMinOn (↑toDual ∘ f) s adual.comp_mapsTo: ∀ {α : Type ?u.14430} {β : Type ?u.14429} {δ : Type ?u.14428} [inst : Preorder β] {f : α → β} {s : Set α} {a : α}
{t : Set δ} {g : δ → α} {b : δ}, IsMinOn f s a → MapsTo g t s → g b = a → IsMinOn (f ∘ g) t bcomp_mapsTo hg: MapsTo g t shg ha: g b = aha
#align is_max_on.comp_maps_to IsMaxOn.comp_mapsTo: ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set δ} {g : δ → α}
{b : δ}, IsMaxOn f s a → MapsTo g t s → g b = a → IsMaxOn (f ∘ g) t bIsMaxOn.comp_mapsTo

theorem IsExtrOn.comp_mapsTo: ∀ {t : Set δ} {g : δ → α} {b : δ}, IsExtrOn f s a → MapsTo g t s → g b = a → IsExtrOn (f ∘ g) t bIsExtrOn.comp_mapsTo {t: Set δt : Set: Type ?u.14571 → Type ?u.14571Set δ: Type xδ} {g: δ → αg : δ: Type xδ → α: Type uα} {b: δb : δ: Type xδ} (hf: IsExtrOn f s ahf : IsExtrOn: {α : Type ?u.14581} → {β : Type ?u.14580} → [inst : Preorder β] → (α → β) → Set α → α → PropIsExtrOn f: α → βf s: Set αs a: αa)
(hg: MapsTo g t shg : MapsTo: {α : Type ?u.14619} → {β : Type ?u.14618} → (α → β) → Set α → Set β → PropMapsTo g: δ → αg t: Set δt s: Set αs) (```