/-
Copyright (c) 2019 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov

! This file was ported from Lean 3 source module order.filter.extr
! leanprover-community/mathlib commit 1f0096e6caa61e9c849ec2adbd227e960e9dff58
! 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.918
Preorder 
β: Type v
β] [
Preorder: Type ?u.2533 → Type ?u.2533
Preorder 
γ: Type w
γ]

variable (
f: α → β
f : 
α: Type u
α → 
β: Type v
β) (
s: Set α
s : 
Set: Type ?u.4060 → Type ?u.4060
Set 
α: Type u
α) (
l: Filter α
l : 
Filter: Type ?u.1565 → Type ?u.1565
Filter 
α: 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: Prop
IsMinFilter : 
Prop: Type
Prop :=
  ∀ᶠ 
x: ?m.80
x in 
l: Filter α
l, 
f: α → β
f 
a: α
a ≤ 
f: α → β
f 
x: ?m.80
x
#align is_min_filter 
IsMinFilter: {α : Type u} → {β : Type v} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter

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

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

/-- `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 α → α → Prop
IsMinOn :=
  
IsMinFilter: {α : Type ?u.272} → {β : Type ?u.271} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter 
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 α → α → Prop
IsMinOn

/-- `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.352
IsMaxOn :=
  
IsMaxFilter: {α : Type ?u.355} → {β : Type ?u.354} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter 
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 α → α → Prop
IsMaxOn

/-- `IsExtrOn f s a` means `IsMinOn f s a` or `IsMaxOn f s a` -/
def 
IsExtrOn: Prop
IsExtrOn : 
Prop: Type
Prop :=
  
IsExtrFilter: {α : Type ?u.437} → {β : Type ?u.436} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsExtrFilter 
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 α → α → Prop
IsExtrOn

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

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

theorem 
isMinOn_iff: IsMinOn f s a ↔ ∀ (x : α), x ∈ s → f a ≤ f x
isMinOn_iff : 
IsMinOn: {α : Type ?u.717} → {β : Type ?u.716} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn 
f: α → β
f 
s: Set α
s 
a: α
a ↔ ∀ 
x: ?m.731
x ∈ 
s: Set α
s, 
f: α → β
f 
a: α
a ≤ 
f: α → β
f 
x: ?m.731
x :=
  
Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.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 x
isMinOn_iff

theorem 
isMaxOn_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMaxOn f s a ↔ ∀ (x : α), x ∈ s → f x ≤ f a
isMaxOn_iff : 
IsMaxOn: {α : Type ?u.830} → {β : Type ?u.829} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn 
f: α → β
f 
s: Set α
s 
a: α
a ↔ ∀ 
x: ?m.844
x ∈ 
s: Set α
s, 
f: α → β
f 
x: ?m.844
x ≤ 
f: α → β
f 
a: α
a :=
  
Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.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 a
isMaxOn_iff

theorem 
isMinOn_univ_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {a : α}, IsMinOn f univ a ↔ ∀ (x : α), f a ≤ f x
isMinOn_univ_iff : 
IsMinOn: {α : Type ?u.943} → {β : Type ?u.942} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn 
f: α → β
f 
univ: {α : Type ?u.950} → Set α
univ 
a: α
a ↔ ∀ 
x: ?m.959
x, 
f: α → β
f 
a: α
a ≤ 
f: α → β
f 
x: ?m.959
x :=
  
univ_subset_iff: ∀ {α : Type ?u.975} {s : Set α}, univ ⊆ s ↔ s = univ
univ_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 ∈ s
eq_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 x
isMinOn_univ_iff

theorem 
isMaxOn_univ_iff: IsMaxOn f univ a ↔ ∀ (x : α), f x ≤ f a
isMaxOn_univ_iff : 
IsMaxOn: {α : Type ?u.1049} → {β : Type ?u.1048} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn 
f: α → β
f 
univ: {α : Type ?u.1056} → Set α
univ 
a: α
a ↔ ∀ 
x: ?m.1065
x, 
f: α → β
f 
x: ?m.1065
x ≤ 
f: α → β
f 
a: α
a :=
  
univ_subset_iff: ∀ {α : Type ?u.1081} {s : Set α}, univ ⊆ s ↔ s = univ
univ_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 ∈ s
eq_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 a
isMaxOn_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 a
h : 
IsMinFilter: {α : Type ?u.1155} → {β : Type ?u.1154} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter 
f: α → β
f 
l: Filter α
l 
a: α
a) : 
Tendsto: {α : Type ?u.1192} → {β : Type ?u.1191} → (α → β) → Filter α → Filter β → Prop
Tendsto 
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) l
tendsto_principal.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 
h: IsMinFilter f l a
h
#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 a
h : 
IsMaxFilter: {α : Type ?u.1308} → {β : Type ?u.1307} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter 
f: α → β
f 
l: Filter α
l 
a: α
a) : 
Tendsto: {α : Type ?u.1345} → {β : Type ?u.1344} → (α → β) → Filter α → Filter β → Prop
Tendsto 
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) l
tendsto_principal.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 
h: IsMaxFilter f l a
h
#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 a
IsMinFilter.isExtr : 
IsMinFilter: {α : Type ?u.1462} → {β : Type ?u.1461} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter 
f: α → β
f 
l: Filter α
l 
a: α
a → 
IsExtrFilter: {α : Type ?u.1498} → {β : Type ?u.1497} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsExtrFilter 
f: α → β
f 
l: Filter α
l 
a: α
a :=
  
Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.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 a
IsMinFilter.isExtr

theorem 
IsMaxFilter.isExtr: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMaxFilter f l a → IsExtrFilter f l a
IsMaxFilter.isExtr : 
IsMaxFilter: {α : Type ?u.1578} → {β : Type ?u.1577} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter 
f: α → β
f 
l: Filter α
l 
a: α
a → 
IsExtrFilter: {α : Type ?u.1614} → {β : Type ?u.1613} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsExtrFilter 
f: α → β
f 
l: Filter α
l 
a: α
a :=
  
Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.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 a
IsMaxFilter.isExtr

theorem 
IsMinOn.isExtr: IsMinOn f s a → IsExtrOn f s a
IsMinOn.isExtr (
h: IsMinOn f s a
h : 
IsMinOn: {α : Type ?u.1693} → {β : Type ?u.1692} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn 
f: α → β
f 
s: Set α
s 
a: α
a) : 
IsExtrOn: {α : Type ?u.1731} → {β : Type ?u.1730} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsExtrOn 
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 a
IsMinFilter.isExtr 
h: IsMinOn f s a
h
#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 a
IsMinOn.isExtr

theorem 
IsMaxOn.isExtr: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α}, IsMaxOn f s a → IsExtrOn f s a
IsMaxOn.isExtr (
h: IsMaxOn f s a
h : 
IsMaxOn: {α : Type ?u.1845} → {β : Type ?u.1844} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn 
f: α → β
f 
s: Set α
s 
a: α
a) : 
IsExtrOn: {α : Type ?u.1883} → {β : Type ?u.1882} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsExtrOn 
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 a
IsMaxFilter.isExtr 
h: IsMaxOn f s a
h
#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 a
IsMaxOn.isExtr

/-! ### Constant function -/


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

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

theorem 
isExtrFilter_const: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {a : α} {b : β}, IsExtrFilter (fun x => b) l a
isExtrFilter_const {
b: β
b : 
β: Type v
β} : 
IsExtrFilter: {α : Type ?u.2267} → {β : Type ?u.2266} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsExtrFilter (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 a
isMinFilter_const.
isExtr: ∀ {α : Type ?u.2338} {β : Type ?u.2337} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMinFilter f l a → IsExtrFilter f l a
isExtr
#align is_extr_filter_const 
isExtrFilter_const: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {a : α} {b : β}, IsExtrFilter (fun x => b) l a
isExtrFilter_const

theorem 
isMinOn_const: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {s : Set α} {a : α} {b : β}, IsMinOn (fun x => b) s a
isMinOn_const {
b: β
b : 
β: Type v
β} : 
IsMinOn: {α : Type ?u.2435} → {β : Type ?u.2434} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn (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 a
isMinFilter_const
#align is_min_on_const 
isMinOn_const: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {s : Set α} {a : α} {b : β}, IsMinOn (fun x => b) s a
isMinOn_const

theorem 
isMaxOn_const: ∀ {b : β}, IsMaxOn (fun x => b) s a
isMaxOn_const {
b: β
b : 
β: Type v
β} : 
IsMaxOn: {α : Type ?u.2557} → {β : Type ?u.2556} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn (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 a
isMaxFilter_const
#align is_max_on_const 
isMaxOn_const: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {s : Set α} {a : α} {b : β}, IsMaxOn (fun x => b) s a
isMaxOn_const

theorem 
isExtrOn_const: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {s : Set α} {a : α} {b : β}, IsExtrOn (fun x => b) s a
isExtrOn_const {
b: β
b : 
β: Type v
β} : 
IsExtrOn: {α : Type ?u.2679} → {β : Type ?u.2678} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsExtrOn (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 a
isExtrFilter_const
#align is_extr_on_const 
isExtrOn_const: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {s : Set α} {a : α} {b : β}, IsExtrOn (fun x => b) s a
isExtrOn_const

/-! ### Order dual -/


open OrderDual (toDual)

theorem 
isMinFilter_dual_iff: IsMinFilter (↑toDual ∘ f) l a ↔ IsMaxFilter f l a
isMinFilter_dual_iff : 
IsMinFilter: {α : Type ?u.2799} → {β : Type ?u.2798} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter (
toDual: {α : Type ?u.2811} → α ≃ αᵒᵈ
toDual ∘ 
f: α → β
f) 
l: Filter α
l 
a: α
a ↔ 
IsMaxFilter: {α : Type ?u.2921} → {β : Type ?u.2920} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter 
f: α → β
f 
l: Filter α
l 
a: α
a :=
  
Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.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 a
isMinFilter_dual_iff

theorem 
isMaxFilter_dual_iff: IsMaxFilter (↑toDual ∘ f) l a ↔ IsMinFilter f l a
isMaxFilter_dual_iff : 
IsMaxFilter: {α : Type ?u.2985} → {β : Type ?u.2984} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter (
toDual: {α : Type ?u.2997} → α ≃ αᵒᵈ
toDual ∘ 
f: α → β
f) 
l: Filter α
l 
a: α
a ↔ 
IsMinFilter: {α : Type ?u.3107} → {β : Type ?u.3106} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter 
f: α → β
f 
l: Filter α
l 
a: α
a :=
  
Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.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 a
isMaxFilter_dual_iff

theorem 
isExtrFilter_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsExtrFilter (↑toDual ∘ f) l a ↔ IsExtrFilter f l a
isExtrFilter_dual_iff : 
IsExtrFilter: {α : Type ?u.3171} → {β : Type ?u.3170} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsExtrFilter (
toDual: {α : Type ?u.3183} → α ≃ αᵒᵈ
toDual ∘ 
f: α → β
f) 
l: Filter α
l 
a: α
a ↔ 
IsExtrFilter: {α : Type ?u.3293} → {β : Type ?u.3292} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsExtrFilter 
f: α → β
f 
l: Filter α
l 
a: α
a :=
  
or_comm: ∀ {a b : Prop}, a ∨ b ↔ b ∨ a
or_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 a
isExtrFilter_dual_iff

alias 
isMinFilter_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMinFilter (↑toDual ∘ f) l a ↔ IsMaxFilter f l a
isMinFilter_dual_iff ↔ 
IsMinFilter.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMinFilter (↑toDual ∘ f) l a → IsMaxFilter f l a
IsMinFilter.undual 
IsMaxFilter.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMaxFilter f l a → IsMinFilter (↑toDual ∘ f) l a
IsMaxFilter.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 a
IsMinFilter.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 a
IsMaxFilter.dual

alias 
isMaxFilter_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMaxFilter (↑toDual ∘ f) l a ↔ IsMinFilter f l a
isMaxFilter_dual_iff ↔ 
IsMaxFilter.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMaxFilter (↑toDual ∘ f) l a → IsMinFilter f l a
IsMaxFilter.undual 
IsMinFilter.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMinFilter f l a → IsMaxFilter (↑toDual ∘ f) l a
IsMinFilter.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 a
IsMaxFilter.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 a
IsMinFilter.dual

alias 
isExtrFilter_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsExtrFilter (↑toDual ∘ f) l a ↔ IsExtrFilter f l a
isExtrFilter_dual_iff ↔ 
IsExtrFilter.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsExtrFilter (↑toDual ∘ f) l a → IsExtrFilter f l a
IsExtrFilter.undual 
IsExtrFilter.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsExtrFilter f l a → IsExtrFilter (↑toDual ∘ f) l a
IsExtrFilter.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 a
IsExtrFilter.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 a
IsExtrFilter.dual

theorem 
isMinOn_dual_iff: IsMinOn (↑toDual ∘ f) s a ↔ IsMaxOn f s a
isMinOn_dual_iff : 
IsMinOn: {α : Type ?u.3434} → {β : Type ?u.3433} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn (
toDual: {α : Type ?u.3446} → α ≃ αᵒᵈ
toDual ∘ 
f: α → β
f) 
s: Set α
s 
a: α
a ↔ 
IsMaxOn: {α : Type ?u.3557} → {β : Type ?u.3556} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn 
f: α → β
f 
s: Set α
s 
a: α
a :=
  
Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.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 a
isMinOn_dual_iff

theorem 
isMaxOn_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMaxOn (↑toDual ∘ f) s a ↔ IsMinOn f s a
isMaxOn_dual_iff : 
IsMaxOn: {α : Type ?u.3622} → {β : Type ?u.3621} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn (
toDual: {α : Type ?u.3634} → α ≃ αᵒᵈ
toDual ∘ 
f: α → β
f) 
s: Set α
s 
a: α
a ↔ 
IsMinOn: {α : Type ?u.3745} → {β : Type ?u.3744} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn 
f: α → β
f 
s: Set α
s 
a: α
a :=
  
Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.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 a
isMaxOn_dual_iff

theorem 
isExtrOn_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsExtrOn (↑toDual ∘ f) s a ↔ IsExtrOn f s a
isExtrOn_dual_iff : 
IsExtrOn: {α : Type ?u.3810} → {β : Type ?u.3809} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsExtrOn (
toDual: {α : Type ?u.3822} → α ≃ αᵒᵈ
toDual ∘ 
f: α → β
f) 
s: Set α
s 
a: α
a ↔ 
IsExtrOn: {α : Type ?u.3933} → {β : Type ?u.3932} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsExtrOn 
f: α → β
f 
s: Set α
s 
a: α
a :=
  
or_comm: ∀ {a b : Prop}, a ∨ b ↔ b ∨ a
or_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 a
isExtrOn_dual_iff

alias 
isMinOn_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMinOn (↑toDual ∘ f) s a ↔ IsMaxOn f s a
isMinOn_dual_iff ↔ 
IsMinOn.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMinOn (↑toDual ∘ f) s a → IsMaxOn f s a
IsMinOn.undual 
IsMaxOn.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMaxOn f s a → IsMinOn (↑toDual ∘ f) s a
IsMaxOn.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 a
IsMinOn.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 a
IsMaxOn.dual

alias 
isMaxOn_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMaxOn (↑toDual ∘ f) s a ↔ IsMinOn f s a
isMaxOn_dual_iff ↔ 
IsMaxOn.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMaxOn (↑toDual ∘ f) s a → IsMinOn f s a
IsMaxOn.undual 
IsMinOn.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMinOn f s a → IsMaxOn (↑toDual ∘ f) s a
IsMinOn.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 a
IsMaxOn.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 a
IsMinOn.dual

alias 
isExtrOn_dual_iff: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsExtrOn (↑toDual ∘ f) s a ↔ IsExtrOn f s a
isExtrOn_dual_iff ↔ 
IsExtrOn.undual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsExtrOn (↑toDual ∘ f) s a → IsExtrOn f s a
IsExtrOn.undual 
IsExtrOn.dual: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsExtrOn f s a → IsExtrOn (↑toDual ∘ f) s a
IsExtrOn.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 a
IsExtrOn.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 a
IsExtrOn.dual

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


theorem 
IsMinFilter.filter_mono: IsMinFilter f l a → l' ≤ l → IsMinFilter f l' a
IsMinFilter.filter_mono (
h: IsMinFilter f l a
h : 
IsMinFilter: {α : Type ?u.4075} → {β : Type ?u.4074} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter 
f: α → β
f 
l: Filter α
l 
a: α
a) (
hl: l' ≤ l
hl : 
l': Filter α
l' ≤ 
l: Filter α
l) : 
IsMinFilter: {α : Type ?u.4148} → {β : Type ?u.4147} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter 
f: α → β
f 
l': Filter α
l' 
a: α
a :=
  
hl: l' ≤ l
hl 
h: IsMinFilter f l a
h
#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' a
IsMinFilter.filter_mono

theorem 
IsMaxFilter.filter_mono: IsMaxFilter f l a → l' ≤ l → IsMaxFilter f l' a
IsMaxFilter.filter_mono (
h: IsMaxFilter f l a
h : 
IsMaxFilter: {α : Type ?u.4234} → {β : Type ?u.4233} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter 
f: α → β
f 
l: Filter α
l 
a: α
a) (
hl: l' ≤ l
hl : 
l': Filter α
l' ≤ 
l: Filter α
l) : 
IsMaxFilter: {α : Type ?u.4307} → {β : Type ?u.4306} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter 
f: α → β
f 
l': Filter α
l' 
a: α
a :=
  
hl: l' ≤ l
hl 
h: IsMaxFilter f l a
h
#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' a
IsMaxFilter.filter_mono

theorem 
IsExtrFilter.filter_mono: IsExtrFilter f l a → l' ≤ l → IsExtrFilter f l' a
IsExtrFilter.filter_mono (
h: IsExtrFilter f l a
h : 
IsExtrFilter: {α : Type ?u.4393} → {β : Type ?u.4392} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsExtrFilter 
f: α → β
f 
l: Filter α
l 
a: α
a) (
hl: l' ≤ l
hl : 
l': Filter α
l' ≤ 
l: Filter α
l) : 
IsExtrFilter: {α : Type ?u.4466} → {β : Type ?u.4465} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsExtrFilter 
f: α → β
f 
l': Filter α
l' 
a: α
a :=
  
h: IsExtrFilter f l a
h.
elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c
elim (fun 
h: ?m.4512
h => (
h: ?m.4512
h.
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' a
filter_mono 
hl: l' ≤ l
hl).
isExtr: ∀ {α : Type ?u.4545} {β : Type ?u.4544} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMinFilter f l a → IsExtrFilter f l a
isExtr) fun 
h: ?m.4570
h => (
h: ?m.4570
h.
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' a
filter_mono 
hl: l' ≤ l
hl).
isExtr: ∀ {α : Type ?u.4599} {β : Type ?u.4598} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMaxFilter f l a → IsExtrFilter f l a
isExtr
#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' a
IsExtrFilter.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') a
IsMinFilter.filter_inf (
h: IsMinFilter f l a
h : 
IsMinFilter: {α : Type ?u.4662} → {β : Type ?u.4661} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter 
f: α → β
f 
l: Filter α
l 
a: α
a) (
l': Filter α
l') : 
IsMinFilter: {α : Type ?u.4702} → {β : Type ?u.4701} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter 
f: α → β
f (
l: Filter α
l ⊓ 
l': ?m.4698
l') 
a: α
a :=
  
h: IsMinFilter f l a
h.
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' a
filter_mono 
inf_le_left: ∀ {α : Type ?u.4793} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ a
inf_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') a
IsMinFilter.filter_inf

theorem 
IsMaxFilter.filter_inf: IsMaxFilter f l a → ∀ (l' : Filter α), IsMaxFilter f (l ⊓ l') a
IsMaxFilter.filter_inf (
h: IsMaxFilter f l a
h : 
IsMaxFilter: {α : Type ?u.4933} → {β : Type ?u.4932} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter 
f: α → β
f 
l: Filter α
l 
a: α
a) (
l': ?m.4969
l') : 
IsMaxFilter: {α : Type ?u.4973} → {β : Type ?u.4972} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter 
f: α → β
f (
l: Filter α
l ⊓ 
l': ?m.4969
l') 
a: α
a :=
  
h: IsMaxFilter f l a
h.
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' a
filter_mono 
inf_le_left: ∀ {α : Type ?u.5064} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ a
inf_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') a
IsMaxFilter.filter_inf

theorem 
IsExtrFilter.filter_inf: IsExtrFilter f l a → ∀ (l' : Filter α), IsExtrFilter f (l ⊓ l') a
IsExtrFilter.filter_inf (
h: IsExtrFilter f l a
h : 
IsExtrFilter: {α : Type ?u.5204} → {β : Type ?u.5203} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsExtrFilter 
f: α → β
f 
l: Filter α
l 
a: α
a) (
l': ?m.5240
l') : 
IsExtrFilter: {α : Type ?u.5244} → {β : Type ?u.5243} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsExtrFilter 
f: α → β
f (
l: Filter α
l ⊓ 
l': ?m.5240
l') 
a: α
a :=
  
h: IsExtrFilter f l a
h.
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' a
filter_mono 
inf_le_left: ∀ {α : Type ?u.5335} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ a
inf_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') a
IsExtrFilter.filter_inf

theorem 
IsMinOn.on_subset: IsMinOn f t a → s ⊆ t → IsMinOn f s a
IsMinOn.on_subset (
hf: IsMinOn f t a
hf : 
IsMinOn: {α : Type ?u.5475} → {β : Type ?u.5474} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn 
f: α → β
f 
t: Set α
t 
a: α
a) (
h: s ⊆ t
h : 
s: Set α
s ⊆ 
t: Set α
t) : 
IsMinOn: {α : Type ?u.5533} → {β : Type ?u.5532} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn 
f: α → β
f 
s: Set α
s 
a: α
a :=
  
hf: IsMinOn f t a
hf.
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' a
filter_mono <| 
principal_mono: ∀ {α : Type ?u.5595} {s t : Set α}, 𝓟 s ≤ 𝓟 t ↔ s ⊆ t
principal_mono.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 
h: s ⊆ t
h
#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 a
IsMinOn.on_subset

theorem 
IsMaxOn.on_subset: IsMaxOn f t a → s ⊆ t → IsMaxOn f s a
IsMaxOn.on_subset (
hf: IsMaxOn f t a
hf : 
IsMaxOn: {α : Type ?u.5662} → {β : Type ?u.5661} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn 
f: α → β
f 
t: Set α
t 
a: α
a) (
h: s ⊆ t
h : 
s: Set α
s ⊆ 
t: Set α
t) : 
IsMaxOn: {α : Type ?u.5720} → {β : Type ?u.5719} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn 
f: α → β
f 
s: Set α
s 
a: α
a :=
  
hf: IsMaxOn f t a
hf.
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' a
filter_mono <| 
principal_mono: ∀ {α : Type ?u.5782} {s t : Set α}, 𝓟 s ≤ 𝓟 t ↔ s ⊆ t
principal_mono.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 
h: s ⊆ t
h
#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 a
IsMaxOn.on_subset

theorem 
IsExtrOn.on_subset: IsExtrOn f t a → s ⊆ t → IsExtrOn f s a
IsExtrOn.on_subset (
hf: IsExtrOn f t a
hf : 
IsExtrOn: {α : Type ?u.5849} → {β : Type ?u.5848} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsExtrOn 
f: α → β
f 
t: Set α
t 
a: α
a) (
h: s ⊆ t
h : 
s: Set α
s ⊆ 
t: Set α
t) : 
IsExtrOn: {α : Type ?u.5907} → {β : Type ?u.5906} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsExtrOn 
f: α → β
f 
s: Set α
s 
a: α
a :=
  
hf: IsExtrOn f t a
hf.
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' a
filter_mono <| 
principal_mono: ∀ {α : Type ?u.5969} {s t : Set α}, 𝓟 s ≤ 𝓟 t ↔ s ⊆ t
principal_mono.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 
h: s ⊆ t
h
#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 a
IsExtrOn.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) a
IsMinOn.inter (
hf: IsMinOn f s a
hf : 
IsMinOn: {α : Type ?u.6036} → {β : Type ?u.6035} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn 
f: α → β
f 
s: Set α
s 
a: α
a) (
t: ?m.6073
t) : 
IsMinOn: {α : Type ?u.6077} → {β : Type ?u.6076} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn 
f: α → β
f (
s: Set α
s ∩ 
t: ?m.6073
t) 
a: α
a :=
  
hf: IsMinOn f s a
hf.
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 a
on_subset (
inter_subset_left: ∀ {α : Type ?u.6160} (s t : Set α), s ∩ t ⊆ s
inter_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) a
IsMinOn.inter

theorem 
IsMaxOn.inter: ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMaxOn f s a → ∀ (t : Set α), IsMaxOn f (s ∩ t) a
IsMaxOn.inter (
hf: IsMaxOn f s a
hf : 
IsMaxOn: {α : Type ?u.6208} → {β : Type ?u.6207} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn 
f: α → β
f 
s: Set α
s 
a: α
a) (
t: ?m.6245
t) : 
IsMaxOn: {α : Type ?u.6249} → {β : Type ?u.6248} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn 
f: α → β
f (
s: Set α
s ∩ 
t: ?m.6245
t) 
a: α
a :=
  
hf: IsMaxOn f s a
hf.
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 a
on_subset (
inter_subset_left: ∀ {α : Type ?u.6332} (s t : Set α), s ∩ t ⊆ s
inter_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) a
IsMaxOn.inter

theorem 
IsExtrOn.inter: IsExtrOn f s a → ∀ (t : Set α), IsExtrOn f (s ∩ t) a
IsExtrOn.inter (
hf: IsExtrOn f s a
hf : 
IsExtrOn: {α : Type ?u.6380} → {β : Type ?u.6379} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsExtrOn 
f: α → β
f 
s: Set α
s 
a: α
a) (
t: ?m.6417
t) : 
IsExtrOn: {α : Type ?u.6421} → {β : Type ?u.6420} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsExtrOn 
f: α → β
f (
s: Set α
s ∩ 
t: ?m.6417
t) 
a: α
a :=
  
hf: IsExtrOn f s a
hf.
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 a
on_subset (
inter_subset_left: ∀ {α : Type ?u.6500} (s t : Set α), s ∩ t ⊆ s
inter_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) a
IsExtrOn.inter

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


theorem 
IsMinFilter.comp_mono: IsMinFilter f l a → ∀ {g : β → γ}, Monotone g → IsMinFilter (g ∘ f) l a
IsMinFilter.comp_mono (
hf: IsMinFilter f l a
hf : 
IsMinFilter: {α : Type ?u.6548} → {β : Type ?u.6547} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter 
f: α → β
f 
l: Filter α
l 
a: α
a) {
g: β → γ
g : 
β: Type v
β → 
γ: Type w
γ} (
hg: Monotone g
hg : 
Monotone: {α : Type ?u.6589} → {β : Type ?u.6588} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone 
g: β → γ
g) :
    
IsMinFilter: {α : Type ?u.6648} → {β : Type ?u.6647} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter (
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 ∈ f
mem_of_superset 
hf: IsMinFilter f l a
hf fun 
_x: ?m.6712
_x 
hx: ?m.6715
hx => 
hg: Monotone g
hg 
hx: ?m.6715
hx
#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 a
IsMinFilter.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
IsMaxFilter.comp_mono (
hf: IsMaxFilter f l a
hf : 
IsMaxFilter: {α : Type ?u.6779} → {β : Type ?u.6778} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter 
f: α → β
f 
l: Filter α
l 
a: α
a) {
g: β → γ
g : 
β: Type v
β → 
γ: Type w
γ} (
hg: Monotone g
hg : 
Monotone: {α : Type ?u.6820} → {β : Type ?u.6819} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone 
g: β → γ
g) :
    
IsMaxFilter: {α : Type ?u.6879} → {β : Type ?u.6878} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter (
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 ∈ f
mem_of_superset 
hf: IsMaxFilter f l a
hf fun 
_x: ?m.6943
_x 
hx: ?m.6946
hx => 
hg: Monotone g
hg 
hx: ?m.6946
hx
#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 a
IsMaxFilter.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
IsExtrFilter.comp_mono (
hf: IsExtrFilter f l a
hf : 
IsExtrFilter: {α : Type ?u.7010} → {β : Type ?u.7009} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsExtrFilter 
f: α → β
f 
l: Filter α
l 
a: α
a) {
g: β → γ
g : 
β: Type v
β → 
γ: Type w
γ} (
hg: Monotone g
hg : 
Monotone: {α : Type ?u.7051} → {β : Type ?u.7050} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone 
g: β → γ
g) :
    
IsExtrFilter: {α : Type ?u.7110} → {β : Type ?u.7109} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsExtrFilter (
g: β → γ
g ∘ 
f: α → β
f) 
l: Filter α
l 
a: α
a :=
  
hf: IsExtrFilter f l a
hf.
elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c
elim (fun 
hf: ?m.7172
hf => (
hf: ?m.7172
hf.
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 a
comp_mono 
hg: Monotone g
hg).
isExtr: ∀ {α : Type ?u.7219} {β : Type ?u.7218} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMinFilter f l a → IsExtrFilter f l a
isExtr) fun 
hf: ?m.7251
hf => (
hf: ?m.7251
hf.
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 a
comp_mono 
hg: Monotone g
hg).
isExtr: ∀ {α : Type ?u.7292} {β : Type ?u.7291} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMaxFilter f l a → IsExtrFilter f l a
isExtr
#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 a
IsExtrFilter.comp_mono

theorem 
IsMinFilter.comp_antitone: IsMinFilter f l a → ∀ {g : β → γ}, Antitone g → IsMaxFilter (g ∘ f) l a
IsMinFilter.comp_antitone (
hf: IsMinFilter f l a
hf : 
IsMinFilter: {α : Type ?u.7365} → {β : Type ?u.7364} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter 
f: α → β
f 
l: Filter α
l 
a: α
a) {
g: β → γ
g : 
β: Type v
β → 
γ: Type w
γ} (
hg: Antitone g
hg : 
Antitone: {α : Type ?u.7406} → {β : Type ?u.7405} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone 
g: β → γ
g) :
    
IsMaxFilter: {α : Type ?u.7465} → {β : Type ?u.7464} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter (
g: β → γ
g ∘ 
f: α → β
f) 
l: Filter α
l 
a: α
a :=
  
hf: IsMinFilter f l a
hf.
dual: ∀ {α : Type ?u.7516} {β : Type ?u.7515} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMinFilter f l a → IsMaxFilter (↑toDual ∘ f) l a
dual.
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 a
comp_mono fun 
_: ?m.7609
_ 
_: ?m.7612
_ 
h: ?m.7615
h => 
hg: Antitone g
hg 
h: ?m.7615
h
#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 a
IsMinFilter.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
IsMaxFilter.comp_antitone (
hf: IsMaxFilter f l a
hf : 
IsMaxFilter: {α : Type ?u.7682} → {β : Type ?u.7681} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter 
f: α → β
f 
l: Filter α
l 
a: α
a) {
g: β → γ
g : 
β: Type v
β → 
γ: Type w
γ} (
hg: Antitone g
hg : 
Antitone: {α : Type ?u.7723} → {β : Type ?u.7722} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone 
g: β → γ
g) :
    
IsMinFilter: {α : Type ?u.7782} → {β : Type ?u.7781} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter (
g: β → γ
g ∘ 
f: α → β
f) 
l: Filter α
l 
a: α
a :=
  
hf: IsMaxFilter f l a
hf.
dual: ∀ {α : Type ?u.7833} {β : Type ?u.7832} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMaxFilter f l a → IsMinFilter (↑toDual ∘ f) l a
dual.
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 a
comp_mono fun 
_: ?m.7926
_ 
_: ?m.7929
_ 
h: ?m.7932
h => 
hg: Antitone g
hg 
h: ?m.7932
h
#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 a
IsMaxFilter.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
IsExtrFilter.comp_antitone (
hf: IsExtrFilter f l a
hf : 
IsExtrFilter: {α : Type ?u.7999} → {β : Type ?u.7998} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsExtrFilter 
f: α → β
f 
l: Filter α
l 
a: α
a) {
g: β → γ
g : 
β: Type v
β → 
γ: Type w
γ} (
hg: Antitone g
hg : 
Antitone: {α : Type ?u.8040} → {β : Type ?u.8039} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone 
g: β → γ
g) :
    
IsExtrFilter: {α : Type ?u.8099} → {β : Type ?u.8098} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsExtrFilter (
g: β → γ
g ∘ 
f: α → β
f) 
l: Filter α
l 
a: α
a :=
  
hf: IsExtrFilter f l a
hf.
dual: ∀ {α : Type ?u.8150} {β : Type ?u.8149} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsExtrFilter f l a → IsExtrFilter (↑toDual ∘ f) l a
dual.
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 a
comp_mono fun 
_: ?m.8236
_ 
_: ?m.8239
_ 
h: ?m.8242
h => 
hg: Antitone g
hg 
h: ?m.8242
h
#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 a
IsExtrFilter.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 a
IsMinOn.comp_mono (
hf: IsMinOn f s a
hf : 
IsMinOn: {α : Type ?u.8309} → {β : Type ?u.8308} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn 
f: α → β
f 
s: Set α
s 
a: α
a) {
g: β → γ
g : 
β: Type v
β → 
γ: Type w
γ} (
hg: Monotone g
hg : 
Monotone: {α : Type ?u.8351} → {β : Type ?u.8350} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone 
g: β → γ
g) :
    
IsMinOn: {α : Type ?u.8410} → {β : Type ?u.8409} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn (
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 a
IsMinFilter.comp_mono 
hf: IsMinOn f s a
hf 
hg: Monotone g
hg
#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 a
IsMinOn.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 a
IsMaxOn.comp_mono (
hf: IsMaxOn f s a
hf : 
IsMaxOn: {α : Type ?u.8574} → {β : Type ?u.8573} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn 
f: α → β
f 
s: Set α
s 
a: α
a) {
g: β → γ
g : 
β: Type v
β → 
γ: Type w
γ} (
hg: Monotone g
hg : 
Monotone: {α : Type ?u.8616} → {β : Type ?u.8615} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone 
g: β → γ
g) :
    
IsMaxOn: {α : Type ?u.8675} → {β : Type ?u.8674} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn (
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 a
IsMaxFilter.comp_mono 
hf: IsMaxOn f s a
hf 
hg: Monotone g
hg
#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 a
IsMaxOn.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 a
IsExtrOn.comp_mono (
hf: IsExtrOn f s a
hf : 
IsExtrOn: {α : Type ?u.8839} → {β : Type ?u.8838} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsExtrOn 
f: α → β
f 
s: Set α
s 
a: α
a) {
g: β → γ
g : 
β: Type v
β → 
γ: Type w
γ} (
hg: Monotone g
hg : 
Monotone: {α : Type ?u.8881} → {β : Type ?u.8880} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone 
g: β → γ
g) :
    
IsExtrOn: {α : Type ?u.8940} → {β : Type ?u.8939} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsExtrOn (
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 a
IsExtrFilter.comp_mono 
hf: IsExtrOn f s a
hf 
hg: Monotone g
hg
#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 a
IsExtrOn.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 a
IsMinOn.comp_antitone (
hf: IsMinOn f s a
hf : 
IsMinOn: {α : Type ?u.9102} → {β : Type ?u.9101} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn 
f: α → β
f 
s: Set α
s 
a: α
a) {
g: β → γ
g : 
β: Type v
β → 
γ: Type w
γ} (
hg: Antitone g
hg : 
Antitone: {α : Type ?u.9144} → {β : Type ?u.9143} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone 
g: β → γ
g) :
    
IsMaxOn: {α : Type ?u.9203} → {β : Type ?u.9202} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn (
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 a
IsMinFilter.comp_antitone 
hf: IsMinOn f s a
hf 
hg: Antitone g
hg
#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 a
IsMinOn.comp_antitone

theorem 
IsMaxOn.comp_antitone: IsMaxOn f s a → ∀ {g : β → γ}, Antitone g → IsMinOn (g ∘ f) s a
IsMaxOn.comp_antitone (
hf: IsMaxOn f s a
hf : 
IsMaxOn: {α : Type ?u.9367} → {β : Type ?u.9366} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn 
f: α → β
f 
s: Set α
s 
a: α
a) {
g: β → γ
g : 
β: Type v
β → 
γ: Type w
γ} (
hg: Antitone g
hg : 
Antitone: {α : Type ?u.9409} → {β : Type ?u.9408} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone 
g: β → γ
g) :
    
IsMinOn: {α : Type ?u.9468} → {β : Type ?u.9467} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn (
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 a
IsMaxFilter.comp_antitone 
hf: IsMaxOn f s a
hf 
hg: Antitone g
hg
#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 a
IsMaxOn.comp_antitone

theorem 
IsExtrOn.comp_antitone: IsExtrOn f s a → ∀ {g : β → γ}, Antitone g → IsExtrOn (g ∘ f) s a
IsExtrOn.comp_antitone (
hf: IsExtrOn f s a
hf : 
IsExtrOn: {α : Type ?u.9632} → {β : Type ?u.9631} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsExtrOn 
f: α → β
f 
s: Set α
s 
a: α
a) {
g: β → γ
g : 
β: Type v
β → 
γ: Type w
γ} (
hg: Antitone g
hg : 
Antitone: {α : Type ?u.9674} → {β : Type ?u.9673} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone 
g: β → γ
g) :
    
IsExtrOn: {α : Type ?u.9733} → {β : Type ?u.9732} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsExtrOn (
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 a
IsExtrFilter.comp_antitone 
hf: IsExtrOn f s a
hf 
hg: Antitone g
hg
#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 a
IsExtrOn.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 a
IsMinFilter.bicomp_mono [
Preorder: Type ?u.9894 → Type ?u.9894
Preorder 
δ: 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 op
hop : (
(· ≤ ·): β → β → Prop
(· ≤ ·) ⇒ 
(· ≤ ·): γ → γ → Prop
(· ≤ ·) ⇒ 
(· ≤ ·): δ → δ → Prop
(· ≤ ·)) 
op: β → γ → δ
op 
op: β → γ → δ
op) (
hf: IsMinFilter f l a
hf : 
IsMinFilter: {α : Type ?u.10153} → {β : Type ?u.10152} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter 
f: α → β
f 
l: Filter α
l 
a: α
a) {
g: α → γ
g : 
α: Type u
α → 
γ: Type w
γ}
    (
hg: IsMinFilter g l a
hg : 
IsMinFilter: {α : Type ?u.10194} → {β : Type ?u.10193} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter 
g: α → γ
g 
l: Filter α
l 
a: α
a) : 
IsMinFilter: {α : Type ?u.10230} → {β : Type ?u.10229} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter (fun 
x: ?m.10257
x => 
op: β → γ → δ
op (
f: α → β
f 
x: ?m.10257
x) (
g: α → γ
g 
x: ?m.10257
x)) 
l: Filter α
l 
a: α
a :=
  
mem_of_superset: ∀ {α : Type ?u.10314} {f : Filter α} {x y : Set α}, x ∈ f → x ⊆ y → y ∈ f
mem_of_superset (
inter_mem: ∀ {α : Type ?u.10327} {f : Filter α} {s t : Set α}, s ∈ f → t ∈ f → s ∩ t ∈ f
inter_mem 
hf: IsMinFilter f l a
hf 
hg: IsMinFilter g l a
hg) 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 op
hop 
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 a
IsMinFilter.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
IsMaxFilter.bicomp_mono [
Preorder: Type ?u.10554 → Type ?u.10554
Preorder 
δ: 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 op
hop : (
(· ≤ ·): β → β → Prop
(· ≤ ·) ⇒ 
(· ≤ ·): γ → γ → Prop
(· ≤ ·) ⇒ 
(· ≤ ·): δ → δ → Prop
(· ≤ ·)) 
op: β → γ → δ
op 
op: β → γ → δ
op) (
hf: IsMaxFilter f l a
hf : 
IsMaxFilter: {α : Type ?u.10813} → {β : Type ?u.10812} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter 
f: α → β
f 
l: Filter α
l 
a: α
a) {
g: α → γ
g : 
α: Type u
α → 
γ: Type w
γ}
    (
hg: IsMaxFilter g l a
hg : 
IsMaxFilter: {α : Type ?u.10854} → {β : Type ?u.10853} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter 
g: α → γ
g 
l: Filter α
l 
a: α
a) : 
IsMaxFilter: {α : Type ?u.10890} → {β : Type ?u.10889} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter (fun 
x: ?m.10917
x => 
op: β → γ → δ
op (
f: α → β
f 
x: ?m.10917
x) (
g: α → γ
g 
x: ?m.10917
x)) 
l: Filter α
l 
a: α
a :=
  
mem_of_superset: ∀ {α : Type ?u.10974} {f : Filter α} {x y : Set α}, x ∈ f → x ⊆ y → y ∈ f
mem_of_superset (
inter_mem: ∀ {α : Type ?u.10987} {f : Filter α} {s t : Set α}, s ∈ f → t ∈ f → s ∩ t ∈ f
inter_mem 
hf: IsMaxFilter f l a
hf 
hg: IsMaxFilter g l a
hg) 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 op
hop 
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 a
IsMaxFilter.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 a
IsMinOn.bicomp_mono [
Preorder: Type ?u.11214 → Type ?u.11214
Preorder 
δ: 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 op
hop : (
(· ≤ ·): β → β → Prop
(· ≤ ·) ⇒ 
(· ≤ ·): γ → γ → Prop
(· ≤ ·) ⇒ 
(· ≤ ·): δ → δ → Prop
(· ≤ ·)) 
op: β → γ → δ
op 
op: β → γ → δ
op) (
hf: IsMinOn f s a
hf : 
IsMinOn: {α : Type ?u.11473} → {β : Type ?u.11472} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn 
f: α → β
f 
s: Set α
s 
a: α
a) {
g: α → γ
g : 
α: Type u
α → 
γ: Type w
γ}
    (
hg: IsMinOn g s a
hg : 
IsMinOn: {α : Type ?u.11515} → {β : Type ?u.11514} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn 
g: α → γ
g 
s: Set α
s 
a: α
a) : 
IsMinOn: {α : Type ?u.11552} → {β : Type ?u.11551} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn (fun 
x: ?m.11579
x => 
op: β → γ → δ
op (
f: α → β
f 
x: ?m.11579
x) (
g: α → γ
g 
x: ?m.11579
x)) 
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 a
IsMinFilter.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 op
hop 
hf: IsMinOn f s a
hf 
hg: IsMinOn g s a
hg
#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 a
IsMinOn.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 a
IsMaxOn.bicomp_mono [
Preorder: Type ?u.11814 → Type ?u.11814
Preorder 
δ: 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 op
hop : (
(· ≤ ·): β → β → Prop
(· ≤ ·) ⇒ 
(· ≤ ·): γ → γ → Prop
(· ≤ ·) ⇒ 
(· ≤ ·): δ → δ → Prop
(· ≤ ·)) 
op: β → γ → δ
op 
op: β → γ → δ
op) (
hf: IsMaxOn f s a
hf : 
IsMaxOn: {α : Type ?u.12073} → {β : Type ?u.12072} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn 
f: α → β
f 
s: Set α
s 
a: α
a) {
g: α → γ
g : 
α: Type u
α → 
γ: Type w
γ}
    (
hg: IsMaxOn g s a
hg : 
IsMaxOn: {α : Type ?u.12115} → {β : Type ?u.12114} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn 
g: α → γ
g 
s: Set α
s 
a: α
a) : 
IsMaxOn: {α : Type ?u.12152} → {β : Type ?u.12151} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn (fun 
x: ?m.12179
x => 
op: β → γ → δ
op (
f: α → β
f 
x: ?m.12179
x) (
g: α → γ
g 
x: ?m.12179
x)) 
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 a
IsMaxFilter.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 op
hop 
hf: IsMaxOn f s a
hf 
hg: IsMaxOn g s a
hg
#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 a
IsMaxOn.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' b
IsMinFilter.comp_tendsto {
g: δ → α
g : 
δ: Type x
δ → 
α: Type u
α} {
l': Filter δ
l' : 
Filter: Type ?u.12418 → Type ?u.12418
Filter 
δ: Type x
δ} {
b: δ
b : 
δ: Type x
δ} (
hf: IsMinFilter f l (g b)
hf : 
IsMinFilter: {α : Type ?u.12424} → {β : Type ?u.12423} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter 
f: α → β
f 
l: Filter α
l (
g: δ → α
g 
b: δ
b))
    (
hg: Tendsto g l' l
hg : 
Tendsto: {α : Type ?u.12461} → {β : Type ?u.12460} → (α → β) → Filter α → Filter β → Prop
Tendsto 
g: δ → α
g 
l': Filter δ
l' 
l: Filter α
l) : 
IsMinFilter: {α : Type ?u.12471} → {β : Type ?u.12470} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMinFilter (
f: α → β
f ∘ 
g: δ → α
g) 
l': Filter δ
l' 
b: δ
b :=
  
hg: Tendsto g l' l
hg 
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' b
IsMinFilter.comp_tendsto

theorem 
IsMaxFilter.comp_tendsto: ∀ {g : δ → α} {l' : Filter δ} {b : δ}, IsMaxFilter f l (g b) → Tendsto g l' l → IsMaxFilter (f ∘ g) l' b
IsMaxFilter.comp_tendsto {
g: δ → α
g : 
δ: Type x
δ → 
α: Type u
α} {
l': Filter δ
l' : 
Filter: Type ?u.12627 → Type ?u.12627
Filter 
δ: Type x
δ} {
b: δ
b : 
δ: Type x
δ} (
hf: IsMaxFilter f l (g b)
hf : 
IsMaxFilter: {α : Type ?u.12633} → {β : Type ?u.12632} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter 
f: α → β
f 
l: Filter α
l (
g: δ → α
g 
b: δ
b))
    (
hg: Tendsto g l' l
hg : 
Tendsto: {α : Type ?u.12670} → {β : Type ?u.12669} → (α → β) → Filter α → Filter β → Prop
Tendsto 
g: δ → α
g 
l': Filter δ
l' 
l: Filter α
l) : 
IsMaxFilter: {α : Type ?u.12680} → {β : Type ?u.12679} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsMaxFilter (
f: α → β
f ∘ 
g: δ → α
g) 
l': Filter δ
l' 
b: δ
b :=
  
hg: Tendsto g l' l
hg 
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' b
IsMaxFilter.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' b
IsExtrFilter.comp_tendsto {
g: δ → α
g : 
δ: Type x
δ → 
α: Type u
α} {
l': Filter δ
l' : 
Filter: Type ?u.12836 → Type ?u.12836
Filter 
δ: Type x
δ} {
b: δ
b : 
δ: Type x
δ} (
hf: IsExtrFilter f l (g b)
hf : 
IsExtrFilter: {α : Type ?u.12842} → {β : Type ?u.12841} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsExtrFilter 
f: α → β
f 
l: Filter α
l (
g: δ → α
g 
b: δ
b))
    (
hg: Tendsto g l' l
hg : 
Tendsto: {α : Type ?u.12879} → {β : Type ?u.12878} → (α → β) → Filter α → Filter β → Prop
Tendsto 
g: δ → α
g 
l': Filter δ
l' 
l: Filter α
l) : 
IsExtrFilter: {α : Type ?u.12889} → {β : Type ?u.12888} → [inst : Preorder β] → (α → β) → Filter α → α → Prop
IsExtrFilter (
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) → c
elim (fun 
hf: ?m.12955
hf => (
hf: ?m.12955
hf.
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' b
comp_tendsto 
hg: Tendsto g l' l
hg).
isExtr: ∀ {α : Type ?u.12996} {β : Type ?u.12995} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMinFilter f l a → IsExtrFilter f l a
isExtr) fun 
hf: ?m.13028
hf => (
hf: ?m.13028
hf.
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' b
comp_tendsto 
hg: Tendsto g l' l
hg).
isExtr: ∀ {α : Type ?u.13063} {β : Type ?u.13062} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMaxFilter f l a → IsExtrFilter f l a
isExtr
#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' b
IsExtrFilter.comp_tendsto

theorem 
IsMinOn.on_preimage: ∀ (g : δ → α) {b : δ}, IsMinOn f s (g b) → IsMinOn (f ∘ g) (g ⁻¹' s) b
IsMinOn.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 α → α → Prop
IsMinOn 
f: α → β
f 
s: Set α
s (
g: δ → α
g 
b: δ
b)) :
    
IsMinOn: {α : Type ?u.13180} → {β : Type ?u.13179} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn (
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' b
comp_tendsto (
tendsto_principal_principal: ∀ {α : Type ?u.13283} {β : Type ?u.13282} {f : α → β} {s : Set α} {t : Set β},
  Tendsto f (𝓟 s) (𝓟 t) ↔ ∀ (a : α), a ∈ s → f a ∈ t
tendsto_principal_principal.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr <| 
Subset.refl: ∀ {α : Type ?u.13312} (a : Set α), a ⊆ a
Subset.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) b
IsMinOn.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) b
IsMaxOn.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 α → α → Prop
IsMaxOn 
f: α → β
f 
s: Set α
s (
g: δ → α
g 
b: δ
b)) :
    
IsMaxOn: {α : Type ?u.13423} → {β : Type ?u.13422} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn (
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' b
comp_tendsto (
tendsto_principal_principal: ∀ {α : Type ?u.13526} {β : Type ?u.13525} {f : α → β} {s : Set α} {t : Set β},
  Tendsto f (𝓟 s) (𝓟 t) ↔ ∀ (a : α), a ∈ s → f a ∈ t
tendsto_principal_principal.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr <| 
Subset.refl: ∀ {α : Type ?u.13555} (a : Set α), a ⊆ a
Subset.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) b
IsMaxOn.on_preimage

theorem 
IsExtrOn.on_preimage: ∀ (g : δ → α) {b : δ}, IsExtrOn f s (g b) → IsExtrOn (f ∘ g) (g ⁻¹' s) b
IsExtrOn.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 α → α → Prop
IsExtrOn 
f: α → β
f 
s: Set α
s (
g: δ → α
g 
b: δ
b)) :
    
IsExtrOn: {α : Type ?u.13666} → {β : Type ?u.13665} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsExtrOn (
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) → p
elim (fun 
hf: ?m.13756
hf => (
hf: ?m.13756
hf.
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) b
on_preimage 
g: δ → α
g).
isExtr: ∀ {α : Type ?u.13793} {β : Type ?u.13792} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMinOn f s a → IsExtrOn f s a
isExtr) fun 
hf: ?m.13827
hf => (
hf: ?m.13827
hf.
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) b
on_preimage 
g: δ → α
g).
isExtr: ∀ {α : Type ?u.13863} {β : Type ?u.13862} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMaxOn f s a → IsExtrOn f s a
isExtr
#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) b
IsExtrOn.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 b
IsMinOn.comp_mapsTo {
t: Set δ
t : 
Set: Type ?u.13934 → Type ?u.13934
Set 
δ: Type x
δ} {
g: δ → α
g : 
δ: Type x
δ → 
α: Type u
α} {
b: δ
b : 
δ: Type x
δ} (
hf: IsMinOn f s a
hf : 
IsMinOn: {α : Type ?u.13944} → {β : Type ?u.13943} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn 
f: α → β
f 
s: Set α
s 
a: α
a) (
hg: MapsTo g t s
hg : 
MapsTo: {α : Type ?u.13982} → {β : Type ?u.13981} → (α → β) → Set α → Set β → Prop
MapsTo 
g: δ → α
g 
t: Set δ
t 
s: Set α
s)
    (
ha: g b = a
ha : 
g: δ → α
g 
b: δ
b = 
a: α
a) : 
IsMinOn: {α : Type ?u.13998} → {β : Type ?u.13997} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMinOn (
f: α → β
f ∘ 
g: δ → α
g) 
t: Set δ
t 
b: δ
b := fun 
y: ?m.14056
y 
hy: ?m.14059
hy => by
Goals accomplished! 🐙
  
α: Type u

β: Type v

γ: Type w

δ: Type x

inst✝¹: Preorder β

inst✝: Preorder γ

f: α → β

s: Set α

l: Filter α

a: α

t✝: Set α

l': Filter α

t: Set δ

g: δ → α

b: δ

hf: IsMinOn f s a

hg: MapsTo g t s

ha: g b = a

y: δ

hy: y ∈ t

y ∈ { x | (fun x => (f ∘ g) b ≤ (f ∘ g) x) x }simpa only [
ha: g b = a
ha, (· ∘ ·)] using 
hf: IsMinOn f s a
hf (
hg: MapsTo g t s
hg 
hy: y ∈ t
hy)
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 b
IsMinOn.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 b
IsMaxOn.comp_mapsTo {
t: Set δ
t : 
Set: Type ?u.14290 → Type ?u.14290
Set 
δ: Type x
δ} {
g: δ → α
g : 
δ: Type x
δ → 
α: Type u
α} {
b: δ
b : 
δ: Type x
δ} (
hf: IsMaxOn f s a
hf : 
IsMaxOn: {α : Type ?u.14300} → {β : Type ?u.14299} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn 
f: α → β
f 
s: Set α
s 
a: α
a) (
hg: MapsTo g t s
hg : 
MapsTo: {α : Type ?u.14338} → {β : Type ?u.14337} → (α → β) → Set α → Set β → Prop
MapsTo 
g: δ → α
g 
t: Set δ
t 
s: Set α
s)
    (
ha: g b = a
ha : 
g: δ → α
g 
b: δ
b = 
a: α
a) : 
IsMaxOn: {α : Type ?u.14354} → {β : Type ?u.14353} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsMaxOn (
f: α → β
f ∘ 
g: δ → α
g) 
t: Set δ
t 
b: δ
b :=
  
hf: IsMaxOn f s a
hf.
dual: ∀ {α : Type ?u.14412} {β : Type ?u.14411} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMaxOn f s a → IsMinOn (↑toDual ∘ f) s a
dual.
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 b
comp_mapsTo 
hg: MapsTo g t s
hg 
ha: g b = a
ha
#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 b
IsMaxOn.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 b
IsExtrOn.comp_mapsTo {
t: Set δ
t : 
Set: Type ?u.14571 → Type ?u.14571
Set 
δ: Type x
δ} {
g: δ → α
g : 
δ: Type x
δ → 
α: Type u
α} {
b: δ
b : 
δ: Type x
δ} (
hf: IsExtrOn f s a
hf : 
IsExtrOn: {α : Type ?u.14581} → {β : Type ?u.14580} → [inst : Preorder β] → (α → β) → Set α → α → Prop
IsExtrOn 
f: α → β
f 
s: Set α
s 
a: α
a)
    (
hg: MapsTo g t s
hg : 
MapsTo: {α : Type ?u.14619} → {β : Type ?u.14618} → (α → β) → Set α → Set β → Prop
MapsTo 
g: δ → α
g 
t: Set δ
t 
s: Set α
s) (