-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathData.List.Extrema.html
249 lines (189 loc) · 132 KB
/
Data.List.Extrema.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Data.List.Extrema</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">------------------------------------------------------------------------</a>
<a id="74" class="Comment">-- The Agda standard library</a>
<a id="103" class="Comment">--</a>
<a id="106" class="Comment">-- Finding the maximum/minimum values in a list</a>
<a id="154" class="Comment">------------------------------------------------------------------------</a>
<a id="228" class="Symbol">{-#</a> <a id="232" class="Keyword">OPTIONS</a> <a id="240" class="Pragma">--without-K</a> <a id="252" class="Pragma">--safe</a> <a id="259" class="Symbol">#-}</a>
<a id="264" class="Keyword">open</a> <a id="269" class="Keyword">import</a> <a id="276" href="Relation.Binary.html" class="Module">Relation.Binary</a> <a id="292" class="Keyword">using</a> <a id="298" class="Symbol">(</a><a id="299" href="Relation.Binary.Bundles.html#5467" class="Record">TotalOrder</a><a id="309" class="Symbol">;</a> <a id="311" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a><a id="317" class="Symbol">)</a>
<a id="320" class="Keyword">module</a> <a id="327" href="Data.List.Extrema.html" class="Module">Data.List.Extrema</a>
<a id="347" class="Symbol">{</a><a id="348" href="Data.List.Extrema.html#348" class="Bound">b</a> <a id="350" href="Data.List.Extrema.html#350" class="Bound">ℓ₁</a> <a id="353" href="Data.List.Extrema.html#353" class="Bound">ℓ₂</a><a id="355" class="Symbol">}</a> <a id="357" class="Symbol">(</a><a id="358" href="Data.List.Extrema.html#358" class="Bound">totalOrder</a> <a id="369" class="Symbol">:</a> <a id="371" href="Relation.Binary.Bundles.html#5467" class="Record">TotalOrder</a> <a id="382" href="Data.List.Extrema.html#348" class="Bound">b</a> <a id="384" href="Data.List.Extrema.html#350" class="Bound">ℓ₁</a> <a id="387" href="Data.List.Extrema.html#353" class="Bound">ℓ₂</a><a id="389" class="Symbol">)</a> <a id="391" class="Keyword">where</a>
<a id="398" class="Keyword">import</a> <a id="405" href="Algebra.Construct.NaturalChoice.Min.html" class="Module">Algebra.Construct.NaturalChoice.Min</a> <a id="441" class="Symbol">as</a> <a id="444" class="Module">Min</a>
<a id="448" class="Keyword">import</a> <a id="455" href="Algebra.Construct.NaturalChoice.Max.html" class="Module">Algebra.Construct.NaturalChoice.Max</a> <a id="491" class="Symbol">as</a> <a id="494" class="Module">Max</a>
<a id="498" class="Keyword">open</a> <a id="503" class="Keyword">import</a> <a id="510" href="Data.List.Base.html" class="Module">Data.List.Base</a> <a id="525" class="Keyword">using</a> <a id="531" class="Symbol">(</a><a id="532" href="Agda.Builtin.List.html#148" class="Datatype">List</a><a id="536" class="Symbol">;</a> <a id="538" href="Data.List.Base.html#4192" class="Function">foldr</a><a id="543" class="Symbol">)</a>
<a id="545" class="Keyword">open</a> <a id="550" class="Keyword">import</a> <a id="557" href="Data.List.Relation.Unary.Any.html" class="Module">Data.List.Relation.Unary.Any</a> <a id="586" class="Symbol">as</a> <a id="589" class="Module">Any</a> <a id="593" class="Keyword">using</a> <a id="599" class="Symbol">(</a><a id="600" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a><a id="603" class="Symbol">;</a> <a id="605" href="Data.List.Relation.Unary.Any.html#1219" class="InductiveConstructor">here</a><a id="609" class="Symbol">;</a> <a id="611" href="Data.List.Relation.Unary.Any.html#1272" class="InductiveConstructor">there</a><a id="616" class="Symbol">)</a>
<a id="618" class="Keyword">open</a> <a id="623" class="Keyword">import</a> <a id="630" href="Data.List.Relation.Unary.All.html" class="Module">Data.List.Relation.Unary.All</a> <a id="659" class="Keyword">using</a> <a id="665" class="Symbol">(</a><a id="666" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a><a id="669" class="Symbol">;</a> <a id="671" href="Data.List.Relation.Unary.All.html#1507" class="InductiveConstructor">[]</a><a id="673" class="Symbol">;</a> <a id="675" href="Data.List.Relation.Unary.All.html#1524" class="InductiveConstructor Operator">_∷_</a><a id="678" class="Symbol">;</a> <a id="680" href="Data.List.Relation.Unary.All.html#5766" class="Function">lookup</a><a id="686" class="Symbol">;</a> <a id="688" href="Data.List.Relation.Unary.All.html#2935" class="Function">map</a><a id="691" class="Symbol">;</a> <a id="693" href="Data.List.Relation.Unary.All.html#3725" class="Function">tabulate</a><a id="701" class="Symbol">)</a>
<a id="703" class="Keyword">open</a> <a id="708" class="Keyword">import</a> <a id="715" href="Data.List.Membership.Propositional.html" class="Module">Data.List.Membership.Propositional</a> <a id="750" class="Keyword">using</a> <a id="756" class="Symbol">(</a><a id="757" href="Data.List.Membership.Setoid.html#887" class="Function Operator">_∈_</a><a id="760" class="Symbol">;</a> <a id="762" href="Data.List.Membership.Propositional.html#1052" class="Function">lose</a><a id="766" class="Symbol">)</a>
<a id="768" class="Keyword">open</a> <a id="773" class="Keyword">import</a> <a id="780" href="Data.List.Membership.Propositional.Properties.html" class="Module">Data.List.Membership.Propositional.Properties</a>
<a id="828" class="Keyword">using</a> <a id="834" class="Symbol">(</a><a id="835" href="Data.List.Membership.Propositional.Properties.html#11319" class="Function">foldr-selective</a><a id="850" class="Symbol">)</a>
<a id="852" class="Keyword">open</a> <a id="857" class="Keyword">import</a> <a id="864" href="Data.List.Relation.Binary.Subset.Propositional.html" class="Module">Data.List.Relation.Binary.Subset.Propositional</a> <a id="911" class="Keyword">using</a> <a id="917" class="Symbol">(</a><a id="918" href="Data.List.Relation.Binary.Subset.Setoid.html#739" class="Function Operator">_⊆_</a><a id="921" class="Symbol">;</a> <a id="923" href="Data.List.Relation.Binary.Subset.Setoid.html#801" class="Function Operator">_⊇_</a><a id="926" class="Symbol">)</a>
<a id="928" class="Keyword">open</a> <a id="933" class="Keyword">import</a> <a id="940" href="Data.List.Properties.html" class="Module">Data.List.Properties</a>
<a id="961" class="Keyword">open</a> <a id="966" class="Keyword">import</a> <a id="973" href="Data.Sum.Base.html" class="Module">Data.Sum.Base</a> <a id="987" class="Keyword">using</a> <a id="993" class="Symbol">(</a><a id="994" href="Data.Sum.Base.html#734" class="Datatype Operator">_⊎_</a><a id="997" class="Symbol">;</a> <a id="999" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a><a id="1003" class="Symbol">;</a> <a id="1005" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a><a id="1009" class="Symbol">)</a>
<a id="1011" class="Keyword">open</a> <a id="1016" class="Keyword">import</a> <a id="1023" href="Function.Base.html" class="Module">Function.Base</a> <a id="1037" class="Keyword">using</a> <a id="1043" class="Symbol">(</a><a id="1044" href="Function.Base.html#615" class="Function">id</a><a id="1046" class="Symbol">;</a> <a id="1048" href="Function.Base.html#1554" class="Function">flip</a><a id="1052" class="Symbol">;</a> <a id="1054" href="Function.Base.html#6285" class="Function Operator">_on_</a><a id="1058" class="Symbol">;</a> <a id="1060" href="Function.Base.html#1031" class="Function Operator">_∘_</a><a id="1063" class="Symbol">)</a>
<a id="1065" class="Keyword">open</a> <a id="1070" class="Keyword">import</a> <a id="1077" href="Level.html" class="Module">Level</a> <a id="1083" class="Keyword">using</a> <a id="1089" class="Symbol">(</a><a id="1090" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="1095" class="Symbol">)</a>
<a id="1097" class="Keyword">open</a> <a id="1102" class="Keyword">import</a> <a id="1109" href="Relation.Unary.html" class="Module">Relation.Unary</a> <a id="1124" class="Keyword">using</a> <a id="1130" class="Symbol">(</a><a id="1131" href="Relation.Unary.html#1101" class="Function">Pred</a><a id="1135" class="Symbol">)</a>
<a id="1137" class="Keyword">import</a> <a id="1144" href="Relation.Binary.Construct.NonStrictToStrict.html" class="Module">Relation.Binary.Construct.NonStrictToStrict</a> <a id="1188" class="Symbol">as</a> <a id="1191" class="Module">NonStrictToStrict</a>
<a id="1209" class="Keyword">open</a> <a id="1214" class="Keyword">import</a> <a id="1221" href="Relation.Binary.PropositionalEquality.Core.html" class="Module">Relation.Binary.PropositionalEquality.Core</a>
<a id="1266" class="Keyword">using</a> <a id="1272" class="Symbol">(</a><a id="1273" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a><a id="1276" class="Symbol">;</a> <a id="1278" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a><a id="1281" class="Symbol">;</a> <a id="1283" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a><a id="1288" class="Symbol">)</a> <a id="1290" class="Keyword">renaming</a> <a id="1299" class="Symbol">(</a><a id="1300" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1305" class="Symbol">to</a> <a id="1308" class="InductiveConstructor">≡-refl</a><a id="1314" class="Symbol">)</a>
<a id="1316" class="Keyword">import</a> <a id="1323" href="Relation.Binary.Construct.On.html" class="Module">Relation.Binary.Construct.On</a> <a id="1352" class="Symbol">as</a> <a id="1355" class="Module">On</a>
<a id="1359" class="Comment">------------------------------------------------------------------------------</a>
<a id="1438" class="Comment">-- Setup</a>
<a id="1448" class="Keyword">open</a> <a id="1453" href="Relation.Binary.Bundles.html#5467" class="Module">TotalOrder</a> <a id="1464" href="Data.List.Extrema.html#358" class="Bound">totalOrder</a> <a id="1475" class="Keyword">renaming</a> <a id="1484" class="Symbol">(</a><a id="1485" href="Relation.Binary.Bundles.html#5548" class="Field">Carrier</a> <a id="1493" class="Symbol">to</a> <a id="1496" class="Field">B</a><a id="1497" class="Symbol">)</a>
<a id="1499" class="Keyword">open</a> <a id="1504" href="Relation.Binary.Construct.NonStrictToStrict.html" class="Module">NonStrictToStrict</a> <a id="1522" href="Relation.Binary.Bundles.html#5573" class="Field Operator">_≈_</a> <a id="1526" href="Relation.Binary.Bundles.html#5607" class="Field Operator">_≤_</a> <a id="1530" class="Keyword">using</a> <a id="1536" class="Symbol">(</a><a id="1537" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator">_<_</a><a id="1540" class="Symbol">)</a>
<a id="1542" class="Keyword">open</a> <a id="1547" class="Keyword">import</a> <a id="1554" href="Data.List.Extrema.Core.html" class="Module">Data.List.Extrema.Core</a> <a id="1577" href="Data.List.Extrema.html#358" class="Bound">totalOrder</a>
<a id="1590" class="Keyword">renaming</a> <a id="1599" class="Symbol">(</a><a id="1600" href="Data.List.Extrema.Core.html#2003" class="Function">⊓ᴸ</a> <a id="1603" class="Symbol">to</a> <a id="1606" class="Function">⊓-lift</a><a id="1612" class="Symbol">;</a> <a id="1614" href="Data.List.Extrema.Core.html#2049" class="Function">⊔ᴸ</a> <a id="1617" class="Symbol">to</a> <a id="1620" class="Function">⊔-lift</a><a id="1626" class="Symbol">)</a>
<a id="1629" class="Keyword">private</a>
<a id="1639" class="Keyword">variable</a>
<a id="1652" href="Data.List.Extrema.html#1652" class="Generalizable">a</a> <a id="1654" href="Data.List.Extrema.html#1654" class="Generalizable">p</a> <a id="1656" class="Symbol">:</a> <a id="1658" href="Agda.Primitive.html#597" class="Postulate">Level</a>
<a id="1668" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="1670" class="Symbol">:</a> <a id="1672" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1676" href="Data.List.Extrema.html#1652" class="Generalizable">a</a>
<a id="1679" class="Comment">------------------------------------------------------------------------------</a>
<a id="1758" class="Comment">-- Functions</a>
<a id="argmin"></a><a id="1772" href="Data.List.Extrema.html#1772" class="Function">argmin</a> <a id="1779" class="Symbol">:</a> <a id="1781" class="Symbol">(</a><a id="1782" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="1784" class="Symbol">→</a> <a id="1786" href="Data.List.Extrema.html#1496" class="Field">B</a><a id="1787" class="Symbol">)</a> <a id="1789" class="Symbol">→</a> <a id="1791" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="1793" class="Symbol">→</a> <a id="1795" href="Agda.Builtin.List.html#148" class="Datatype">List</a> <a id="1800" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="1802" class="Symbol">→</a> <a id="1804" href="Data.List.Extrema.html#1668" class="Generalizable">A</a>
<a id="1806" href="Data.List.Extrema.html#1772" class="Function">argmin</a> <a id="1813" href="Data.List.Extrema.html#1813" class="Bound">f</a> <a id="1815" class="Symbol">=</a> <a id="1817" href="Data.List.Base.html#4192" class="Function">foldr</a> <a id="1823" class="Symbol">(</a><a id="1824" href="Data.List.Extrema.html#1606" class="Function">⊓-lift</a> <a id="1831" href="Data.List.Extrema.html#1813" class="Bound">f</a><a id="1832" class="Symbol">)</a>
<a id="argmax"></a><a id="1835" href="Data.List.Extrema.html#1835" class="Function">argmax</a> <a id="1842" class="Symbol">:</a> <a id="1844" class="Symbol">(</a><a id="1845" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="1847" class="Symbol">→</a> <a id="1849" href="Data.List.Extrema.html#1496" class="Field">B</a><a id="1850" class="Symbol">)</a> <a id="1852" class="Symbol">→</a> <a id="1854" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="1856" class="Symbol">→</a> <a id="1858" href="Agda.Builtin.List.html#148" class="Datatype">List</a> <a id="1863" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="1865" class="Symbol">→</a> <a id="1867" href="Data.List.Extrema.html#1668" class="Generalizable">A</a>
<a id="1869" href="Data.List.Extrema.html#1835" class="Function">argmax</a> <a id="1876" href="Data.List.Extrema.html#1876" class="Bound">f</a> <a id="1878" class="Symbol">=</a> <a id="1880" href="Data.List.Base.html#4192" class="Function">foldr</a> <a id="1886" class="Symbol">(</a><a id="1887" href="Data.List.Extrema.html#1620" class="Function">⊔-lift</a> <a id="1894" href="Data.List.Extrema.html#1876" class="Bound">f</a><a id="1895" class="Symbol">)</a>
<a id="min"></a><a id="1898" href="Data.List.Extrema.html#1898" class="Function">min</a> <a id="1902" class="Symbol">:</a> <a id="1904" href="Data.List.Extrema.html#1496" class="Field">B</a> <a id="1906" class="Symbol">→</a> <a id="1908" href="Agda.Builtin.List.html#148" class="Datatype">List</a> <a id="1913" href="Data.List.Extrema.html#1496" class="Field">B</a> <a id="1915" class="Symbol">→</a> <a id="1917" href="Data.List.Extrema.html#1496" class="Field">B</a>
<a id="1919" href="Data.List.Extrema.html#1898" class="Function">min</a> <a id="1923" class="Symbol">=</a> <a id="1925" href="Data.List.Extrema.html#1772" class="Function">argmin</a> <a id="1932" href="Function.Base.html#615" class="Function">id</a>
<a id="max"></a><a id="1936" href="Data.List.Extrema.html#1936" class="Function">max</a> <a id="1940" class="Symbol">:</a> <a id="1942" href="Data.List.Extrema.html#1496" class="Field">B</a> <a id="1944" class="Symbol">→</a> <a id="1946" href="Agda.Builtin.List.html#148" class="Datatype">List</a> <a id="1951" href="Data.List.Extrema.html#1496" class="Field">B</a> <a id="1953" class="Symbol">→</a> <a id="1955" href="Data.List.Extrema.html#1496" class="Field">B</a>
<a id="1957" href="Data.List.Extrema.html#1936" class="Function">max</a> <a id="1961" class="Symbol">=</a> <a id="1963" href="Data.List.Extrema.html#1835" class="Function">argmax</a> <a id="1970" href="Function.Base.html#615" class="Function">id</a>
<a id="1974" class="Comment">------------------------------------------------------------------------------</a>
<a id="2053" class="Comment">-- Properties of argmin</a>
<a id="2078" class="Keyword">module</a> <a id="2085" href="Data.List.Extrema.html#2085" class="Module">_</a> <a id="2087" class="Symbol">{</a><a id="2088" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2090" class="Symbol">:</a> <a id="2092" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="2094" class="Symbol">→</a> <a id="2096" href="Data.List.Extrema.html#1496" class="Field">B</a><a id="2097" class="Symbol">}</a> <a id="2099" class="Keyword">where</a>
<a id="2108" href="Data.List.Extrema.html#2108" class="Function">f[argmin]≤v⁺</a> <a id="2121" class="Symbol">:</a> <a id="2123" class="Symbol">∀</a> <a id="2125" class="Symbol">{</a><a id="2126" href="Data.List.Extrema.html#2126" class="Bound">v</a><a id="2127" class="Symbol">}</a> <a id="2129" href="Data.List.Extrema.html#2129" class="Bound">⊤</a> <a id="2131" href="Data.List.Extrema.html#2131" class="Bound">xs</a> <a id="2134" class="Symbol">→</a> <a id="2136" class="Symbol">(</a><a id="2137" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2139" href="Data.List.Extrema.html#2129" class="Bound">⊤</a> <a id="2141" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="2143" href="Data.List.Extrema.html#2126" class="Bound">v</a><a id="2144" class="Symbol">)</a> <a id="2146" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="2148" class="Symbol">(</a><a id="2149" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="2153" class="Symbol">(λ</a> <a id="2156" href="Data.List.Extrema.html#2156" class="Bound">x</a> <a id="2158" class="Symbol">→</a> <a id="2160" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2162" href="Data.List.Extrema.html#2156" class="Bound">x</a> <a id="2164" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="2166" href="Data.List.Extrema.html#2126" class="Bound">v</a><a id="2167" class="Symbol">)</a> <a id="2169" href="Data.List.Extrema.html#2131" class="Bound">xs</a><a id="2171" class="Symbol">)</a> <a id="2173" class="Symbol">→</a>
<a id="2191" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2193" class="Symbol">(</a><a id="2194" href="Data.List.Extrema.html#1772" class="Function">argmin</a> <a id="2201" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2203" href="Data.List.Extrema.html#2129" class="Bound">⊤</a> <a id="2205" href="Data.List.Extrema.html#2131" class="Bound">xs</a><a id="2207" class="Symbol">)</a> <a id="2209" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="2211" href="Data.List.Extrema.html#2126" class="Bound">v</a>
<a id="2215" href="Data.List.Extrema.html#2108" class="Function">f[argmin]≤v⁺</a> <a id="2228" class="Symbol">=</a> <a id="2230" href="Data.List.Properties.html#17762" class="Function">foldr-preservesᵒ</a> <a id="2247" class="Symbol">(</a><a id="2248" href="Data.List.Extrema.Core.html#2272" class="Function">⊓ᴸ-presᵒ-≤v</a> <a id="2260" href="Data.List.Extrema.html#2088" class="Bound">f</a><a id="2261" class="Symbol">)</a>
<a id="2266" href="Data.List.Extrema.html#2266" class="Function">f[argmin]<v⁺</a> <a id="2279" class="Symbol">:</a> <a id="2281" class="Symbol">∀</a> <a id="2283" class="Symbol">{</a><a id="2284" href="Data.List.Extrema.html#2284" class="Bound">v</a><a id="2285" class="Symbol">}</a> <a id="2287" href="Data.List.Extrema.html#2287" class="Bound">⊤</a> <a id="2289" href="Data.List.Extrema.html#2289" class="Bound">xs</a> <a id="2292" class="Symbol">→</a> <a id="2294" class="Symbol">(</a><a id="2295" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2297" href="Data.List.Extrema.html#2287" class="Bound">⊤</a> <a id="2299" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="2301" href="Data.List.Extrema.html#2284" class="Bound">v</a><a id="2302" class="Symbol">)</a> <a id="2304" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="2306" class="Symbol">(</a><a id="2307" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="2311" class="Symbol">(λ</a> <a id="2314" href="Data.List.Extrema.html#2314" class="Bound">x</a> <a id="2316" class="Symbol">→</a> <a id="2318" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2320" href="Data.List.Extrema.html#2314" class="Bound">x</a> <a id="2322" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="2324" href="Data.List.Extrema.html#2284" class="Bound">v</a><a id="2325" class="Symbol">)</a> <a id="2327" href="Data.List.Extrema.html#2289" class="Bound">xs</a><a id="2329" class="Symbol">)</a> <a id="2331" class="Symbol">→</a>
<a id="2349" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2351" class="Symbol">(</a><a id="2352" href="Data.List.Extrema.html#1772" class="Function">argmin</a> <a id="2359" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2361" href="Data.List.Extrema.html#2287" class="Bound">⊤</a> <a id="2363" href="Data.List.Extrema.html#2289" class="Bound">xs</a><a id="2365" class="Symbol">)</a> <a id="2367" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="2369" href="Data.List.Extrema.html#2284" class="Bound">v</a>
<a id="2373" href="Data.List.Extrema.html#2266" class="Function">f[argmin]<v⁺</a> <a id="2386" class="Symbol">=</a> <a id="2388" href="Data.List.Properties.html#17762" class="Function">foldr-preservesᵒ</a> <a id="2405" class="Symbol">(</a><a id="2406" href="Data.List.Extrema.Core.html#2414" class="Function">⊓ᴸ-presᵒ-<v</a> <a id="2418" href="Data.List.Extrema.html#2088" class="Bound">f</a><a id="2419" class="Symbol">)</a>
<a id="2424" href="Data.List.Extrema.html#2424" class="Function">v≤f[argmin]⁺</a> <a id="2437" class="Symbol">:</a> <a id="2439" class="Symbol">∀</a> <a id="2441" class="Symbol">{</a><a id="2442" href="Data.List.Extrema.html#2442" class="Bound">v</a> <a id="2444" href="Data.List.Extrema.html#2444" class="Bound">⊤</a> <a id="2446" href="Data.List.Extrema.html#2446" class="Bound">xs</a><a id="2448" class="Symbol">}</a> <a id="2450" class="Symbol">→</a> <a id="2452" href="Data.List.Extrema.html#2442" class="Bound">v</a> <a id="2454" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="2456" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2458" href="Data.List.Extrema.html#2444" class="Bound">⊤</a> <a id="2460" class="Symbol">→</a> <a id="2462" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="2466" class="Symbol">(λ</a> <a id="2469" href="Data.List.Extrema.html#2469" class="Bound">x</a> <a id="2471" class="Symbol">→</a> <a id="2473" href="Data.List.Extrema.html#2442" class="Bound">v</a> <a id="2475" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="2477" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2479" href="Data.List.Extrema.html#2469" class="Bound">x</a><a id="2480" class="Symbol">)</a> <a id="2482" href="Data.List.Extrema.html#2446" class="Bound">xs</a> <a id="2485" class="Symbol">→</a>
<a id="2503" href="Data.List.Extrema.html#2442" class="Bound">v</a> <a id="2505" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="2507" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2509" class="Symbol">(</a><a id="2510" href="Data.List.Extrema.html#1772" class="Function">argmin</a> <a id="2517" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2519" href="Data.List.Extrema.html#2444" class="Bound">⊤</a> <a id="2521" href="Data.List.Extrema.html#2446" class="Bound">xs</a><a id="2523" class="Symbol">)</a>
<a id="2527" href="Data.List.Extrema.html#2424" class="Function">v≤f[argmin]⁺</a> <a id="2540" class="Symbol">=</a> <a id="2542" href="Data.List.Properties.html#17289" class="Function">foldr-preservesᵇ</a> <a id="2559" class="Symbol">(</a><a id="2560" href="Data.List.Extrema.Core.html#2556" class="Function">⊓ᴸ-presᵇ-v≤</a> <a id="2572" href="Data.List.Extrema.html#2088" class="Bound">f</a><a id="2573" class="Symbol">)</a>
<a id="2578" href="Data.List.Extrema.html#2578" class="Function">v<f[argmin]⁺</a> <a id="2591" class="Symbol">:</a> <a id="2593" class="Symbol">∀</a> <a id="2595" class="Symbol">{</a><a id="2596" href="Data.List.Extrema.html#2596" class="Bound">v</a> <a id="2598" href="Data.List.Extrema.html#2598" class="Bound">⊤</a> <a id="2600" href="Data.List.Extrema.html#2600" class="Bound">xs</a><a id="2602" class="Symbol">}</a> <a id="2604" class="Symbol">→</a> <a id="2606" href="Data.List.Extrema.html#2596" class="Bound">v</a> <a id="2608" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="2610" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2612" href="Data.List.Extrema.html#2598" class="Bound">⊤</a> <a id="2614" class="Symbol">→</a> <a id="2616" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="2620" class="Symbol">(λ</a> <a id="2623" href="Data.List.Extrema.html#2623" class="Bound">x</a> <a id="2625" class="Symbol">→</a> <a id="2627" href="Data.List.Extrema.html#2596" class="Bound">v</a> <a id="2629" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="2631" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2633" href="Data.List.Extrema.html#2623" class="Bound">x</a><a id="2634" class="Symbol">)</a> <a id="2636" href="Data.List.Extrema.html#2600" class="Bound">xs</a> <a id="2639" class="Symbol">→</a>
<a id="2657" href="Data.List.Extrema.html#2596" class="Bound">v</a> <a id="2659" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="2661" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2663" class="Symbol">(</a><a id="2664" href="Data.List.Extrema.html#1772" class="Function">argmin</a> <a id="2671" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2673" href="Data.List.Extrema.html#2598" class="Bound">⊤</a> <a id="2675" href="Data.List.Extrema.html#2600" class="Bound">xs</a><a id="2677" class="Symbol">)</a>
<a id="2681" href="Data.List.Extrema.html#2578" class="Function">v<f[argmin]⁺</a> <a id="2694" class="Symbol">=</a> <a id="2696" href="Data.List.Properties.html#17289" class="Function">foldr-preservesᵇ</a> <a id="2713" class="Symbol">(</a><a id="2714" href="Data.List.Extrema.Core.html#2700" class="Function">⊓ᴸ-presᵇ-v<</a> <a id="2726" href="Data.List.Extrema.html#2088" class="Bound">f</a><a id="2727" class="Symbol">)</a>
<a id="2732" href="Data.List.Extrema.html#2732" class="Function">f[argmin]≤f[⊤]</a> <a id="2747" class="Symbol">:</a> <a id="2749" class="Symbol">∀</a> <a id="2751" href="Data.List.Extrema.html#2751" class="Bound">⊤</a> <a id="2753" href="Data.List.Extrema.html#2753" class="Bound">xs</a> <a id="2756" class="Symbol">→</a> <a id="2758" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2760" class="Symbol">(</a><a id="2761" href="Data.List.Extrema.html#1772" class="Function">argmin</a> <a id="2768" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2770" href="Data.List.Extrema.html#2751" class="Bound">⊤</a> <a id="2772" href="Data.List.Extrema.html#2753" class="Bound">xs</a><a id="2774" class="Symbol">)</a> <a id="2776" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="2778" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2780" href="Data.List.Extrema.html#2751" class="Bound">⊤</a>
<a id="2784" href="Data.List.Extrema.html#2732" class="Function">f[argmin]≤f[⊤]</a> <a id="2799" href="Data.List.Extrema.html#2799" class="Bound">⊤</a> <a id="2801" href="Data.List.Extrema.html#2801" class="Bound">xs</a> <a id="2804" class="Symbol">=</a> <a id="2806" href="Data.List.Extrema.html#2108" class="Function">f[argmin]≤v⁺</a> <a id="2819" href="Data.List.Extrema.html#2799" class="Bound">⊤</a> <a id="2821" href="Data.List.Extrema.html#2801" class="Bound">xs</a> <a id="2824" class="Symbol">(</a><a id="2825" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="2830" href="Relation.Binary.Structures.html#2438" class="Function">refl</a><a id="2834" class="Symbol">)</a>
<a id="2839" href="Data.List.Extrema.html#2839" class="Function">f[argmin]≤f[xs]</a> <a id="2855" class="Symbol">:</a> <a id="2857" class="Symbol">∀</a> <a id="2859" href="Data.List.Extrema.html#2859" class="Bound">⊤</a> <a id="2861" href="Data.List.Extrema.html#2861" class="Bound">xs</a> <a id="2864" class="Symbol">→</a> <a id="2866" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="2870" class="Symbol">(λ</a> <a id="2873" href="Data.List.Extrema.html#2873" class="Bound">x</a> <a id="2875" class="Symbol">→</a> <a id="2877" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2879" class="Symbol">(</a><a id="2880" href="Data.List.Extrema.html#1772" class="Function">argmin</a> <a id="2887" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2889" href="Data.List.Extrema.html#2859" class="Bound">⊤</a> <a id="2891" href="Data.List.Extrema.html#2861" class="Bound">xs</a><a id="2893" class="Symbol">)</a> <a id="2895" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="2897" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="2899" href="Data.List.Extrema.html#2873" class="Bound">x</a><a id="2900" class="Symbol">)</a> <a id="2902" href="Data.List.Extrema.html#2861" class="Bound">xs</a>
<a id="2907" href="Data.List.Extrema.html#2839" class="Function">f[argmin]≤f[xs]</a> <a id="2923" href="Data.List.Extrema.html#2923" class="Bound">⊤</a> <a id="2925" href="Data.List.Extrema.html#2925" class="Bound">xs</a> <a id="2928" class="Symbol">=</a> <a id="2930" href="Data.List.Properties.html#17016" class="Function">foldr-forcesᵇ</a> <a id="2944" class="Symbol">(</a><a id="2945" href="Data.List.Extrema.Core.html#2844" class="Function">⊓ᴸ-forcesᵇ-v≤</a> <a id="2959" href="Data.List.Extrema.html#2088" class="Bound">f</a><a id="2960" class="Symbol">)</a> <a id="2962" href="Data.List.Extrema.html#2923" class="Bound">⊤</a> <a id="2964" href="Data.List.Extrema.html#2925" class="Bound">xs</a> <a id="2967" href="Relation.Binary.Structures.html#2438" class="Function">refl</a>
<a id="2975" href="Data.List.Extrema.html#2975" class="Function">f[argmin]≈f[v]⁺</a> <a id="2991" class="Symbol">:</a> <a id="2993" class="Symbol">∀</a> <a id="2995" class="Symbol">{</a><a id="2996" href="Data.List.Extrema.html#2996" class="Bound">v</a> <a id="2998" href="Data.List.Extrema.html#2998" class="Bound">⊤</a> <a id="3000" href="Data.List.Extrema.html#3000" class="Bound">xs</a><a id="3002" class="Symbol">}</a> <a id="3004" class="Symbol">→</a> <a id="3006" href="Data.List.Extrema.html#2996" class="Bound">v</a> <a id="3008" href="Data.List.Membership.Setoid.html#887" class="Function Operator">∈</a> <a id="3010" href="Data.List.Extrema.html#3000" class="Bound">xs</a> <a id="3013" class="Symbol">→</a> <a id="3015" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="3019" class="Symbol">(λ</a> <a id="3022" href="Data.List.Extrema.html#3022" class="Bound">x</a> <a id="3024" class="Symbol">→</a> <a id="3026" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="3028" href="Data.List.Extrema.html#2996" class="Bound">v</a> <a id="3030" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="3032" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="3034" href="Data.List.Extrema.html#3022" class="Bound">x</a><a id="3035" class="Symbol">)</a> <a id="3037" href="Data.List.Extrema.html#3000" class="Bound">xs</a> <a id="3040" class="Symbol">→</a> <a id="3042" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="3044" href="Data.List.Extrema.html#2996" class="Bound">v</a> <a id="3046" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="3048" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="3050" href="Data.List.Extrema.html#2998" class="Bound">⊤</a> <a id="3052" class="Symbol">→</a>
<a id="3074" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="3076" class="Symbol">(</a><a id="3077" href="Data.List.Extrema.html#1772" class="Function">argmin</a> <a id="3084" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="3086" href="Data.List.Extrema.html#2998" class="Bound">⊤</a> <a id="3088" href="Data.List.Extrema.html#3000" class="Bound">xs</a><a id="3090" class="Symbol">)</a> <a id="3092" href="Relation.Binary.Bundles.html#5573" class="Field Operator">≈</a> <a id="3094" href="Data.List.Extrema.html#2088" class="Bound">f</a> <a id="3096" href="Data.List.Extrema.html#2996" class="Bound">v</a>
<a id="3100" href="Data.List.Extrema.html#2975" class="Function">f[argmin]≈f[v]⁺</a> <a id="3116" href="Data.List.Extrema.html#3116" class="Bound">v∈xs</a> <a id="3121" href="Data.List.Extrema.html#3121" class="Bound">fv≤fxs</a> <a id="3128" href="Data.List.Extrema.html#3128" class="Bound">fv≤f⊤</a> <a id="3134" class="Symbol">=</a> <a id="3136" href="Relation.Binary.Structures.html#3275" class="Function">antisym</a>
<a id="3148" class="Symbol">(</a><a id="3149" href="Data.List.Extrema.html#2108" class="Function">f[argmin]≤v⁺</a> <a id="3162" class="Symbol">_</a> <a id="3164" class="Symbol">_</a> <a id="3166" class="Symbol">(</a><a id="3167" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="3172" class="Symbol">(</a><a id="3173" href="Data.List.Membership.Propositional.html#1052" class="Function">lose</a> <a id="3178" href="Data.List.Extrema.html#3116" class="Bound">v∈xs</a> <a id="3183" href="Relation.Binary.Structures.html#2438" class="Function">refl</a><a id="3187" class="Symbol">)))</a>
<a id="3195" class="Symbol">(</a><a id="3196" href="Data.List.Extrema.html#2424" class="Function">v≤f[argmin]⁺</a> <a id="3209" href="Data.List.Extrema.html#3128" class="Bound">fv≤f⊤</a> <a id="3215" href="Data.List.Extrema.html#3121" class="Bound">fv≤fxs</a><a id="3221" class="Symbol">)</a>
<a id="argmin[xs]≤argmin[ys]⁺"></a><a id="3224" href="Data.List.Extrema.html#3224" class="Function">argmin[xs]≤argmin[ys]⁺</a> <a id="3247" class="Symbol">:</a> <a id="3249" class="Symbol">∀</a> <a id="3251" class="Symbol">{</a><a id="3252" href="Data.List.Extrema.html#3252" class="Bound">f</a> <a id="3254" href="Data.List.Extrema.html#3254" class="Bound">g</a> <a id="3256" class="Symbol">:</a> <a id="3258" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="3260" class="Symbol">→</a> <a id="3262" href="Data.List.Extrema.html#1496" class="Field">B</a><a id="3263" class="Symbol">}</a> <a id="3265" href="Data.List.Extrema.html#3265" class="Bound">⊤₁</a> <a id="3268" class="Symbol">{</a><a id="3269" href="Data.List.Extrema.html#3269" class="Bound">⊤₂</a><a id="3271" class="Symbol">}</a> <a id="3273" href="Data.List.Extrema.html#3273" class="Bound">xs</a> <a id="3276" class="Symbol">{</a><a id="3277" href="Data.List.Extrema.html#3277" class="Bound">ys</a> <a id="3280" class="Symbol">:</a> <a id="3282" href="Agda.Builtin.List.html#148" class="Datatype">List</a> <a id="3287" href="Data.List.Extrema.html#1668" class="Generalizable">A</a><a id="3288" class="Symbol">}</a> <a id="3290" class="Symbol">→</a>
<a id="3316" class="Symbol">(</a><a id="3317" href="Data.List.Extrema.html#3252" class="Bound">f</a> <a id="3319" href="Data.List.Extrema.html#3265" class="Bound">⊤₁</a> <a id="3322" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="3324" href="Data.List.Extrema.html#3254" class="Bound">g</a> <a id="3326" href="Data.List.Extrema.html#3269" class="Bound">⊤₂</a><a id="3328" class="Symbol">)</a> <a id="3330" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="3332" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="3336" class="Symbol">(λ</a> <a id="3339" href="Data.List.Extrema.html#3339" class="Bound">x</a> <a id="3341" class="Symbol">→</a> <a id="3343" href="Data.List.Extrema.html#3252" class="Bound">f</a> <a id="3345" href="Data.List.Extrema.html#3339" class="Bound">x</a> <a id="3347" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="3349" href="Data.List.Extrema.html#3254" class="Bound">g</a> <a id="3351" href="Data.List.Extrema.html#3269" class="Bound">⊤₂</a><a id="3353" class="Symbol">)</a> <a id="3355" href="Data.List.Extrema.html#3273" class="Bound">xs</a> <a id="3358" class="Symbol">→</a>
<a id="3384" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="3388" class="Symbol">(λ</a> <a id="3391" href="Data.List.Extrema.html#3391" class="Bound">y</a> <a id="3393" class="Symbol">→</a> <a id="3395" class="Symbol">(</a><a id="3396" href="Data.List.Extrema.html#3252" class="Bound">f</a> <a id="3398" href="Data.List.Extrema.html#3265" class="Bound">⊤₁</a> <a id="3401" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="3403" href="Data.List.Extrema.html#3254" class="Bound">g</a> <a id="3405" href="Data.List.Extrema.html#3391" class="Bound">y</a><a id="3406" class="Symbol">)</a> <a id="3408" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="3410" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="3414" class="Symbol">(λ</a> <a id="3417" href="Data.List.Extrema.html#3417" class="Bound">x</a> <a id="3419" class="Symbol">→</a> <a id="3421" href="Data.List.Extrema.html#3252" class="Bound">f</a> <a id="3423" href="Data.List.Extrema.html#3417" class="Bound">x</a> <a id="3425" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="3427" href="Data.List.Extrema.html#3254" class="Bound">g</a> <a id="3429" href="Data.List.Extrema.html#3391" class="Bound">y</a><a id="3430" class="Symbol">)</a> <a id="3432" href="Data.List.Extrema.html#3273" class="Bound">xs</a><a id="3434" class="Symbol">)</a> <a id="3436" href="Data.List.Extrema.html#3277" class="Bound">ys</a> <a id="3439" class="Symbol">→</a>
<a id="3465" href="Data.List.Extrema.html#3252" class="Bound">f</a> <a id="3467" class="Symbol">(</a><a id="3468" href="Data.List.Extrema.html#1772" class="Function">argmin</a> <a id="3475" href="Data.List.Extrema.html#3252" class="Bound">f</a> <a id="3477" href="Data.List.Extrema.html#3265" class="Bound">⊤₁</a> <a id="3480" href="Data.List.Extrema.html#3273" class="Bound">xs</a><a id="3482" class="Symbol">)</a> <a id="3484" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="3486" href="Data.List.Extrema.html#3254" class="Bound">g</a> <a id="3488" class="Symbol">(</a><a id="3489" href="Data.List.Extrema.html#1772" class="Function">argmin</a> <a id="3496" href="Data.List.Extrema.html#3254" class="Bound">g</a> <a id="3498" href="Data.List.Extrema.html#3269" class="Bound">⊤₂</a> <a id="3501" href="Data.List.Extrema.html#3277" class="Bound">ys</a><a id="3503" class="Symbol">)</a>
<a id="3505" href="Data.List.Extrema.html#3224" class="Function">argmin[xs]≤argmin[ys]⁺</a> <a id="3528" href="Data.List.Extrema.html#3528" class="Bound">⊤₁</a> <a id="3531" href="Data.List.Extrema.html#3531" class="Bound">xs</a> <a id="3534" href="Data.List.Extrema.html#3534" class="Bound">xs≤⊤₂</a> <a id="3540" href="Data.List.Extrema.html#3540" class="Bound">xs≤ys</a> <a id="3546" class="Symbol">=</a>
<a id="3550" href="Data.List.Extrema.html#2424" class="Function">v≤f[argmin]⁺</a> <a id="3563" class="Symbol">(</a><a id="3564" href="Data.List.Extrema.html#2108" class="Function">f[argmin]≤v⁺</a> <a id="3577" href="Data.List.Extrema.html#3528" class="Bound">⊤₁</a> <a id="3580" class="Symbol">_</a> <a id="3582" href="Data.List.Extrema.html#3534" class="Bound">xs≤⊤₂</a><a id="3587" class="Symbol">)</a> <a id="3589" class="Symbol">(</a><a id="3590" href="Data.List.Relation.Unary.All.html#2935" class="Function">map</a> <a id="3594" class="Symbol">(</a><a id="3595" href="Data.List.Extrema.html#2108" class="Function">f[argmin]≤v⁺</a> <a id="3608" href="Data.List.Extrema.html#3528" class="Bound">⊤₁</a> <a id="3611" href="Data.List.Extrema.html#3531" class="Bound">xs</a><a id="3613" class="Symbol">)</a> <a id="3615" href="Data.List.Extrema.html#3540" class="Bound">xs≤ys</a><a id="3620" class="Symbol">)</a>
<a id="argmin[xs]<argmin[ys]⁺"></a><a id="3623" href="Data.List.Extrema.html#3623" class="Function">argmin[xs]<argmin[ys]⁺</a> <a id="3646" class="Symbol">:</a> <a id="3648" class="Symbol">∀</a> <a id="3650" class="Symbol">{</a><a id="3651" href="Data.List.Extrema.html#3651" class="Bound">f</a> <a id="3653" href="Data.List.Extrema.html#3653" class="Bound">g</a> <a id="3655" class="Symbol">:</a> <a id="3657" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="3659" class="Symbol">→</a> <a id="3661" href="Data.List.Extrema.html#1496" class="Field">B</a><a id="3662" class="Symbol">}</a> <a id="3664" href="Data.List.Extrema.html#3664" class="Bound">⊤₁</a> <a id="3667" class="Symbol">{</a><a id="3668" href="Data.List.Extrema.html#3668" class="Bound">⊤₂</a><a id="3670" class="Symbol">}</a> <a id="3672" href="Data.List.Extrema.html#3672" class="Bound">xs</a> <a id="3675" class="Symbol">{</a><a id="3676" href="Data.List.Extrema.html#3676" class="Bound">ys</a> <a id="3679" class="Symbol">:</a> <a id="3681" href="Agda.Builtin.List.html#148" class="Datatype">List</a> <a id="3686" href="Data.List.Extrema.html#1668" class="Generalizable">A</a><a id="3687" class="Symbol">}</a> <a id="3689" class="Symbol">→</a>
<a id="3715" class="Symbol">(</a><a id="3716" href="Data.List.Extrema.html#3651" class="Bound">f</a> <a id="3718" href="Data.List.Extrema.html#3664" class="Bound">⊤₁</a> <a id="3721" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="3723" href="Data.List.Extrema.html#3653" class="Bound">g</a> <a id="3725" href="Data.List.Extrema.html#3668" class="Bound">⊤₂</a><a id="3727" class="Symbol">)</a> <a id="3729" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="3731" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="3735" class="Symbol">(λ</a> <a id="3738" href="Data.List.Extrema.html#3738" class="Bound">x</a> <a id="3740" class="Symbol">→</a> <a id="3742" href="Data.List.Extrema.html#3651" class="Bound">f</a> <a id="3744" href="Data.List.Extrema.html#3738" class="Bound">x</a> <a id="3746" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="3748" href="Data.List.Extrema.html#3653" class="Bound">g</a> <a id="3750" href="Data.List.Extrema.html#3668" class="Bound">⊤₂</a><a id="3752" class="Symbol">)</a> <a id="3754" href="Data.List.Extrema.html#3672" class="Bound">xs</a> <a id="3757" class="Symbol">→</a>
<a id="3783" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="3787" class="Symbol">(λ</a> <a id="3790" href="Data.List.Extrema.html#3790" class="Bound">y</a> <a id="3792" class="Symbol">→</a> <a id="3794" class="Symbol">(</a><a id="3795" href="Data.List.Extrema.html#3651" class="Bound">f</a> <a id="3797" href="Data.List.Extrema.html#3664" class="Bound">⊤₁</a> <a id="3800" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="3802" href="Data.List.Extrema.html#3653" class="Bound">g</a> <a id="3804" href="Data.List.Extrema.html#3790" class="Bound">y</a><a id="3805" class="Symbol">)</a> <a id="3807" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="3809" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="3813" class="Symbol">(λ</a> <a id="3816" href="Data.List.Extrema.html#3816" class="Bound">x</a> <a id="3818" class="Symbol">→</a> <a id="3820" href="Data.List.Extrema.html#3651" class="Bound">f</a> <a id="3822" href="Data.List.Extrema.html#3816" class="Bound">x</a> <a id="3824" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="3826" href="Data.List.Extrema.html#3653" class="Bound">g</a> <a id="3828" href="Data.List.Extrema.html#3790" class="Bound">y</a><a id="3829" class="Symbol">)</a> <a id="3831" href="Data.List.Extrema.html#3672" class="Bound">xs</a><a id="3833" class="Symbol">)</a> <a id="3835" href="Data.List.Extrema.html#3676" class="Bound">ys</a> <a id="3838" class="Symbol">→</a>
<a id="3864" href="Data.List.Extrema.html#3651" class="Bound">f</a> <a id="3866" class="Symbol">(</a><a id="3867" href="Data.List.Extrema.html#1772" class="Function">argmin</a> <a id="3874" href="Data.List.Extrema.html#3651" class="Bound">f</a> <a id="3876" href="Data.List.Extrema.html#3664" class="Bound">⊤₁</a> <a id="3879" href="Data.List.Extrema.html#3672" class="Bound">xs</a><a id="3881" class="Symbol">)</a> <a id="3883" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="3885" href="Data.List.Extrema.html#3653" class="Bound">g</a> <a id="3887" class="Symbol">(</a><a id="3888" href="Data.List.Extrema.html#1772" class="Function">argmin</a> <a id="3895" href="Data.List.Extrema.html#3653" class="Bound">g</a> <a id="3897" href="Data.List.Extrema.html#3668" class="Bound">⊤₂</a> <a id="3900" href="Data.List.Extrema.html#3676" class="Bound">ys</a><a id="3902" class="Symbol">)</a>
<a id="3904" href="Data.List.Extrema.html#3623" class="Function">argmin[xs]<argmin[ys]⁺</a> <a id="3927" href="Data.List.Extrema.html#3927" class="Bound">⊤₁</a> <a id="3930" href="Data.List.Extrema.html#3930" class="Bound">xs</a> <a id="3933" href="Data.List.Extrema.html#3933" class="Bound">xs<⊤₂</a> <a id="3939" href="Data.List.Extrema.html#3939" class="Bound">xs<ys</a> <a id="3945" class="Symbol">=</a>
<a id="3949" href="Data.List.Extrema.html#2578" class="Function">v<f[argmin]⁺</a> <a id="3962" class="Symbol">(</a><a id="3963" href="Data.List.Extrema.html#2266" class="Function">f[argmin]<v⁺</a> <a id="3976" href="Data.List.Extrema.html#3927" class="Bound">⊤₁</a> <a id="3979" class="Symbol">_</a> <a id="3981" href="Data.List.Extrema.html#3933" class="Bound">xs<⊤₂</a><a id="3986" class="Symbol">)</a> <a id="3988" class="Symbol">(</a><a id="3989" href="Data.List.Relation.Unary.All.html#2935" class="Function">map</a> <a id="3993" class="Symbol">(</a><a id="3994" href="Data.List.Extrema.html#2266" class="Function">f[argmin]<v⁺</a> <a id="4007" href="Data.List.Extrema.html#3927" class="Bound">⊤₁</a> <a id="4010" href="Data.List.Extrema.html#3930" class="Bound">xs</a><a id="4012" class="Symbol">)</a> <a id="4014" href="Data.List.Extrema.html#3939" class="Bound">xs<ys</a><a id="4019" class="Symbol">)</a>
<a id="argmin-sel"></a><a id="4022" href="Data.List.Extrema.html#4022" class="Function">argmin-sel</a> <a id="4033" class="Symbol">:</a> <a id="4035" class="Symbol">∀</a> <a id="4037" class="Symbol">(</a><a id="4038" href="Data.List.Extrema.html#4038" class="Bound">f</a> <a id="4040" class="Symbol">:</a> <a id="4042" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="4044" class="Symbol">→</a> <a id="4046" href="Data.List.Extrema.html#1496" class="Field">B</a><a id="4047" class="Symbol">)</a> <a id="4049" href="Data.List.Extrema.html#4049" class="Bound">⊤</a> <a id="4051" href="Data.List.Extrema.html#4051" class="Bound">xs</a> <a id="4054" class="Symbol">→</a> <a id="4056" class="Symbol">(</a><a id="4057" href="Data.List.Extrema.html#1772" class="Function">argmin</a> <a id="4064" href="Data.List.Extrema.html#4038" class="Bound">f</a> <a id="4066" href="Data.List.Extrema.html#4049" class="Bound">⊤</a> <a id="4068" href="Data.List.Extrema.html#4051" class="Bound">xs</a> <a id="4071" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="4073" href="Data.List.Extrema.html#4049" class="Bound">⊤</a><a id="4074" class="Symbol">)</a> <a id="4076" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="4078" class="Symbol">(</a><a id="4079" href="Data.List.Extrema.html#1772" class="Function">argmin</a> <a id="4086" href="Data.List.Extrema.html#4038" class="Bound">f</a> <a id="4088" href="Data.List.Extrema.html#4049" class="Bound">⊤</a> <a id="4090" href="Data.List.Extrema.html#4051" class="Bound">xs</a> <a id="4093" href="Data.List.Membership.Setoid.html#887" class="Function Operator">∈</a> <a id="4095" href="Data.List.Extrema.html#4051" class="Bound">xs</a><a id="4097" class="Symbol">)</a>
<a id="4099" href="Data.List.Extrema.html#4022" class="Function">argmin-sel</a> <a id="4110" href="Data.List.Extrema.html#4110" class="Bound">f</a> <a id="4112" class="Symbol">=</a> <a id="4114" href="Data.List.Membership.Propositional.Properties.html#11319" class="Function">foldr-selective</a> <a id="4130" class="Symbol">(</a><a id="4131" href="Data.List.Extrema.Core.html#2189" class="Function">⊓ᴸ-sel</a> <a id="4138" href="Data.List.Extrema.html#4110" class="Bound">f</a><a id="4139" class="Symbol">)</a>
<a id="argmin-all"></a><a id="4142" href="Data.List.Extrema.html#4142" class="Function">argmin-all</a> <a id="4153" class="Symbol">:</a> <a id="4155" class="Symbol">∀</a> <a id="4157" class="Symbol">(</a><a id="4158" href="Data.List.Extrema.html#4158" class="Bound">f</a> <a id="4160" class="Symbol">:</a> <a id="4162" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="4164" class="Symbol">→</a> <a id="4166" href="Data.List.Extrema.html#1496" class="Field">B</a><a id="4167" class="Symbol">)</a> <a id="4169" class="Symbol">{</a><a id="4170" href="Data.List.Extrema.html#4170" class="Bound">⊤</a> <a id="4172" href="Data.List.Extrema.html#4172" class="Bound">xs</a><a id="4174" class="Symbol">}</a> <a id="4176" class="Symbol">{</a><a id="4177" href="Data.List.Extrema.html#4177" class="Bound">P</a> <a id="4179" class="Symbol">:</a> <a id="4181" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4186" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="4188" href="Data.List.Extrema.html#1654" class="Generalizable">p</a><a id="4189" class="Symbol">}</a> <a id="4191" class="Symbol">→</a>
<a id="4206" href="Data.List.Extrema.html#4177" class="Bound">P</a> <a id="4208" href="Data.List.Extrema.html#4170" class="Bound">⊤</a> <a id="4210" class="Symbol">→</a> <a id="4212" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="4216" href="Data.List.Extrema.html#4177" class="Bound">P</a> <a id="4218" href="Data.List.Extrema.html#4172" class="Bound">xs</a> <a id="4221" class="Symbol">→</a> <a id="4223" href="Data.List.Extrema.html#4177" class="Bound">P</a> <a id="4225" class="Symbol">(</a><a id="4226" href="Data.List.Extrema.html#1772" class="Function">argmin</a> <a id="4233" href="Data.List.Extrema.html#4158" class="Bound">f</a> <a id="4235" href="Data.List.Extrema.html#4170" class="Bound">⊤</a> <a id="4237" href="Data.List.Extrema.html#4172" class="Bound">xs</a><a id="4239" class="Symbol">)</a>
<a id="4241" href="Data.List.Extrema.html#4142" class="Function">argmin-all</a> <a id="4252" href="Data.List.Extrema.html#4252" class="Bound">f</a> <a id="4254" class="Symbol">{</a><a id="4255" href="Data.List.Extrema.html#4255" class="Bound">⊤</a><a id="4256" class="Symbol">}</a> <a id="4258" class="Symbol">{</a><a id="4259" href="Data.List.Extrema.html#4259" class="Bound">xs</a><a id="4261" class="Symbol">}</a> <a id="4263" class="Symbol">{</a><a id="4264" class="Argument">P</a> <a id="4266" class="Symbol">=</a> <a id="4268" href="Data.List.Extrema.html#4268" class="Bound">P</a><a id="4269" class="Symbol">}</a> <a id="4272" href="Data.List.Extrema.html#4272" class="Bound">p⊤</a> <a id="4275" href="Data.List.Extrema.html#4275" class="Bound">pxs</a> <a id="4279" class="Keyword">with</a> <a id="4284" href="Data.List.Extrema.html#4022" class="Function">argmin-sel</a> <a id="4295" href="Data.List.Extrema.html#4252" class="Bound">f</a> <a id="4297" href="Data.List.Extrema.html#4255" class="Bound">⊤</a> <a id="4299" href="Data.List.Extrema.html#4259" class="Bound">xs</a>
<a id="4302" class="Symbol">...</a> <a id="4306" class="Symbol">|</a> <a id="4308" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="4313" href="Data.List.Extrema.html#4313" class="Bound">argmin≡⊤</a> <a id="4323" class="Symbol">=</a> <a id="4325" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="4331" class="Bound">P</a> <a id="4333" class="Symbol">(</a><a id="4334" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="4338" href="Data.List.Extrema.html#4313" class="Bound">argmin≡⊤</a><a id="4346" class="Symbol">)</a> <a id="4348" class="Bound">p⊤</a>
<a id="4351" class="Symbol">...</a> <a id="4355" class="Symbol">|</a> <a id="4357" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="4362" href="Data.List.Extrema.html#4362" class="Bound">argmin∈xs</a> <a id="4372" class="Symbol">=</a> <a id="4374" href="Data.List.Relation.Unary.All.html#5766" class="Function">lookup</a> <a id="4381" class="Bound">pxs</a> <a id="4385" href="Data.List.Extrema.html#4362" class="Bound">argmin∈xs</a>
<a id="4396" class="Comment">------------------------------------------------------------------------------</a>
<a id="4475" class="Comment">-- Properties of argmax</a>
<a id="4500" class="Keyword">module</a> <a id="4507" href="Data.List.Extrema.html#4507" class="Module">_</a> <a id="4509" class="Symbol">{</a><a id="4510" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="4512" class="Symbol">:</a> <a id="4514" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="4516" class="Symbol">→</a> <a id="4518" href="Data.List.Extrema.html#1496" class="Field">B</a><a id="4519" class="Symbol">}</a> <a id="4521" class="Keyword">where</a>
<a id="4530" href="Data.List.Extrema.html#4530" class="Function">v≤f[argmax]⁺</a> <a id="4543" class="Symbol">:</a> <a id="4545" class="Symbol">∀</a> <a id="4547" class="Symbol">{</a><a id="4548" href="Data.List.Extrema.html#4548" class="Bound">v</a><a id="4549" class="Symbol">}</a> <a id="4551" href="Data.List.Extrema.html#4551" class="Bound">⊥</a> <a id="4553" href="Data.List.Extrema.html#4553" class="Bound">xs</a> <a id="4556" class="Symbol">→</a> <a id="4558" class="Symbol">(</a><a id="4559" href="Data.List.Extrema.html#4548" class="Bound">v</a> <a id="4561" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="4563" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="4565" href="Data.List.Extrema.html#4551" class="Bound">⊥</a><a id="4566" class="Symbol">)</a> <a id="4568" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="4570" class="Symbol">(</a><a id="4571" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="4575" class="Symbol">(λ</a> <a id="4578" href="Data.List.Extrema.html#4578" class="Bound">x</a> <a id="4580" class="Symbol">→</a> <a id="4582" href="Data.List.Extrema.html#4548" class="Bound">v</a> <a id="4584" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="4586" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="4588" href="Data.List.Extrema.html#4578" class="Bound">x</a><a id="4589" class="Symbol">)</a> <a id="4591" href="Data.List.Extrema.html#4553" class="Bound">xs</a><a id="4593" class="Symbol">)</a> <a id="4595" class="Symbol">→</a>
<a id="4613" href="Data.List.Extrema.html#4548" class="Bound">v</a> <a id="4615" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="4617" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="4619" class="Symbol">(</a><a id="4620" href="Data.List.Extrema.html#1835" class="Function">argmax</a> <a id="4627" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="4629" href="Data.List.Extrema.html#4551" class="Bound">⊥</a> <a id="4631" href="Data.List.Extrema.html#4553" class="Bound">xs</a><a id="4633" class="Symbol">)</a>
<a id="4637" href="Data.List.Extrema.html#4530" class="Function">v≤f[argmax]⁺</a> <a id="4650" class="Symbol">=</a> <a id="4652" href="Data.List.Properties.html#17762" class="Function">foldr-preservesᵒ</a> <a id="4669" class="Symbol">(</a><a id="4670" href="Data.List.Extrema.Core.html#3254" class="Function">⊔ᴸ-presᵒ-v≤</a> <a id="4682" href="Data.List.Extrema.html#4510" class="Bound">f</a><a id="4683" class="Symbol">)</a>
<a id="4688" href="Data.List.Extrema.html#4688" class="Function">v<f[argmax]⁺</a> <a id="4701" class="Symbol">:</a> <a id="4703" class="Symbol">∀</a> <a id="4705" class="Symbol">{</a><a id="4706" href="Data.List.Extrema.html#4706" class="Bound">v</a><a id="4707" class="Symbol">}</a> <a id="4709" href="Data.List.Extrema.html#4709" class="Bound">⊥</a> <a id="4711" href="Data.List.Extrema.html#4711" class="Bound">xs</a> <a id="4714" class="Symbol">→</a> <a id="4716" class="Symbol">(</a><a id="4717" href="Data.List.Extrema.html#4706" class="Bound">v</a> <a id="4719" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="4721" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="4723" href="Data.List.Extrema.html#4709" class="Bound">⊥</a><a id="4724" class="Symbol">)</a> <a id="4726" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="4728" class="Symbol">(</a><a id="4729" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="4733" class="Symbol">(λ</a> <a id="4736" href="Data.List.Extrema.html#4736" class="Bound">x</a> <a id="4738" class="Symbol">→</a> <a id="4740" href="Data.List.Extrema.html#4706" class="Bound">v</a> <a id="4742" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="4744" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="4746" href="Data.List.Extrema.html#4736" class="Bound">x</a><a id="4747" class="Symbol">)</a> <a id="4749" href="Data.List.Extrema.html#4711" class="Bound">xs</a><a id="4751" class="Symbol">)</a> <a id="4753" class="Symbol">→</a>
<a id="4771" href="Data.List.Extrema.html#4706" class="Bound">v</a> <a id="4773" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="4775" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="4777" class="Symbol">(</a><a id="4778" href="Data.List.Extrema.html#1835" class="Function">argmax</a> <a id="4785" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="4787" href="Data.List.Extrema.html#4709" class="Bound">⊥</a> <a id="4789" href="Data.List.Extrema.html#4711" class="Bound">xs</a><a id="4791" class="Symbol">)</a>
<a id="4795" href="Data.List.Extrema.html#4688" class="Function">v<f[argmax]⁺</a> <a id="4808" class="Symbol">=</a> <a id="4810" href="Data.List.Properties.html#17762" class="Function">foldr-preservesᵒ</a> <a id="4827" class="Symbol">(</a><a id="4828" href="Data.List.Extrema.Core.html#3486" class="Function">⊔ᴸ-presᵒ-v<</a> <a id="4840" href="Data.List.Extrema.html#4510" class="Bound">f</a><a id="4841" class="Symbol">)</a>
<a id="4846" href="Data.List.Extrema.html#4846" class="Function">f[argmax]≤v⁺</a> <a id="4859" class="Symbol">:</a> <a id="4861" class="Symbol">∀</a> <a id="4863" class="Symbol">{</a><a id="4864" href="Data.List.Extrema.html#4864" class="Bound">v</a> <a id="4866" href="Data.List.Extrema.html#4866" class="Bound">⊥</a> <a id="4868" href="Data.List.Extrema.html#4868" class="Bound">xs</a><a id="4870" class="Symbol">}</a> <a id="4872" class="Symbol">→</a> <a id="4874" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="4876" href="Data.List.Extrema.html#4866" class="Bound">⊥</a> <a id="4878" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="4880" href="Data.List.Extrema.html#4864" class="Bound">v</a> <a id="4882" class="Symbol">→</a> <a id="4884" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="4888" class="Symbol">(λ</a> <a id="4891" href="Data.List.Extrema.html#4891" class="Bound">x</a> <a id="4893" class="Symbol">→</a> <a id="4895" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="4897" href="Data.List.Extrema.html#4891" class="Bound">x</a> <a id="4899" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="4901" href="Data.List.Extrema.html#4864" class="Bound">v</a><a id="4902" class="Symbol">)</a> <a id="4904" href="Data.List.Extrema.html#4868" class="Bound">xs</a> <a id="4907" class="Symbol">→</a>
<a id="4925" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="4927" class="Symbol">(</a><a id="4928" href="Data.List.Extrema.html#1835" class="Function">argmax</a> <a id="4935" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="4937" href="Data.List.Extrema.html#4866" class="Bound">⊥</a> <a id="4939" href="Data.List.Extrema.html#4868" class="Bound">xs</a><a id="4941" class="Symbol">)</a> <a id="4943" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="4945" href="Data.List.Extrema.html#4864" class="Bound">v</a>
<a id="4949" href="Data.List.Extrema.html#4846" class="Function">f[argmax]≤v⁺</a> <a id="4962" class="Symbol">=</a> <a id="4964" href="Data.List.Properties.html#17289" class="Function">foldr-preservesᵇ</a> <a id="4981" class="Symbol">(</a><a id="4982" href="Data.List.Extrema.Core.html#3724" class="Function">⊔ᴸ-presᵇ-≤v</a> <a id="4994" href="Data.List.Extrema.html#4510" class="Bound">f</a><a id="4995" class="Symbol">)</a>
<a id="5000" href="Data.List.Extrema.html#5000" class="Function">f[argmax]<v⁺</a> <a id="5013" class="Symbol">:</a> <a id="5015" class="Symbol">∀</a> <a id="5017" class="Symbol">{</a><a id="5018" href="Data.List.Extrema.html#5018" class="Bound">v</a> <a id="5020" href="Data.List.Extrema.html#5020" class="Bound">⊥</a> <a id="5022" href="Data.List.Extrema.html#5022" class="Bound">xs</a><a id="5024" class="Symbol">}</a> <a id="5026" class="Symbol">→</a> <a id="5028" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="5030" href="Data.List.Extrema.html#5020" class="Bound">⊥</a> <a id="5032" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="5034" href="Data.List.Extrema.html#5018" class="Bound">v</a> <a id="5036" class="Symbol">→</a> <a id="5038" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="5042" class="Symbol">(λ</a> <a id="5045" href="Data.List.Extrema.html#5045" class="Bound">x</a> <a id="5047" class="Symbol">→</a> <a id="5049" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="5051" href="Data.List.Extrema.html#5045" class="Bound">x</a> <a id="5053" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="5055" href="Data.List.Extrema.html#5018" class="Bound">v</a><a id="5056" class="Symbol">)</a> <a id="5058" href="Data.List.Extrema.html#5022" class="Bound">xs</a> <a id="5061" class="Symbol">→</a>
<a id="5079" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="5081" class="Symbol">(</a><a id="5082" href="Data.List.Extrema.html#1835" class="Function">argmax</a> <a id="5089" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="5091" href="Data.List.Extrema.html#5020" class="Bound">⊥</a> <a id="5093" href="Data.List.Extrema.html#5022" class="Bound">xs</a><a id="5095" class="Symbol">)</a> <a id="5097" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="5099" href="Data.List.Extrema.html#5018" class="Bound">v</a>
<a id="5103" href="Data.List.Extrema.html#5000" class="Function">f[argmax]<v⁺</a> <a id="5116" class="Symbol">=</a> <a id="5118" href="Data.List.Properties.html#17289" class="Function">foldr-preservesᵇ</a> <a id="5135" class="Symbol">(</a><a id="5136" href="Data.List.Extrema.Core.html#3868" class="Function">⊔ᴸ-presᵇ-<v</a> <a id="5148" href="Data.List.Extrema.html#4510" class="Bound">f</a><a id="5149" class="Symbol">)</a>
<a id="5154" href="Data.List.Extrema.html#5154" class="Function">f[⊥]≤f[argmax]</a> <a id="5169" class="Symbol">:</a> <a id="5171" class="Symbol">∀</a> <a id="5173" href="Data.List.Extrema.html#5173" class="Bound">⊥</a> <a id="5175" href="Data.List.Extrema.html#5175" class="Bound">xs</a> <a id="5178" class="Symbol">→</a> <a id="5180" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="5182" href="Data.List.Extrema.html#5173" class="Bound">⊥</a> <a id="5184" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="5186" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="5188" class="Symbol">(</a><a id="5189" href="Data.List.Extrema.html#1835" class="Function">argmax</a> <a id="5196" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="5198" href="Data.List.Extrema.html#5173" class="Bound">⊥</a> <a id="5200" href="Data.List.Extrema.html#5175" class="Bound">xs</a><a id="5202" class="Symbol">)</a>
<a id="5206" href="Data.List.Extrema.html#5154" class="Function">f[⊥]≤f[argmax]</a> <a id="5221" href="Data.List.Extrema.html#5221" class="Bound">⊥</a> <a id="5223" href="Data.List.Extrema.html#5223" class="Bound">xs</a> <a id="5226" class="Symbol">=</a> <a id="5228" href="Data.List.Extrema.html#4530" class="Function">v≤f[argmax]⁺</a> <a id="5241" href="Data.List.Extrema.html#5221" class="Bound">⊥</a> <a id="5243" href="Data.List.Extrema.html#5223" class="Bound">xs</a> <a id="5246" class="Symbol">(</a><a id="5247" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="5252" href="Relation.Binary.Structures.html#2438" class="Function">refl</a><a id="5256" class="Symbol">)</a>
<a id="5261" href="Data.List.Extrema.html#5261" class="Function">f[xs]≤f[argmax]</a> <a id="5277" class="Symbol">:</a> <a id="5279" class="Symbol">∀</a> <a id="5281" href="Data.List.Extrema.html#5281" class="Bound">⊥</a> <a id="5283" href="Data.List.Extrema.html#5283" class="Bound">xs</a> <a id="5286" class="Symbol">→</a> <a id="5288" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="5292" class="Symbol">(λ</a> <a id="5295" href="Data.List.Extrema.html#5295" class="Bound">x</a> <a id="5297" class="Symbol">→</a> <a id="5299" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="5301" href="Data.List.Extrema.html#5295" class="Bound">x</a> <a id="5303" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="5305" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="5307" class="Symbol">(</a><a id="5308" href="Data.List.Extrema.html#1835" class="Function">argmax</a> <a id="5315" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="5317" href="Data.List.Extrema.html#5281" class="Bound">⊥</a> <a id="5319" href="Data.List.Extrema.html#5283" class="Bound">xs</a><a id="5321" class="Symbol">))</a> <a id="5324" href="Data.List.Extrema.html#5283" class="Bound">xs</a>
<a id="5329" href="Data.List.Extrema.html#5261" class="Function">f[xs]≤f[argmax]</a> <a id="5345" href="Data.List.Extrema.html#5345" class="Bound">⊥</a> <a id="5347" href="Data.List.Extrema.html#5347" class="Bound">xs</a> <a id="5350" class="Symbol">=</a> <a id="5352" href="Data.List.Properties.html#17016" class="Function">foldr-forcesᵇ</a> <a id="5366" class="Symbol">(</a><a id="5367" href="Data.List.Extrema.Core.html#4012" class="Function">⊔ᴸ-forcesᵇ-≤v</a> <a id="5381" href="Data.List.Extrema.html#4510" class="Bound">f</a><a id="5382" class="Symbol">)</a> <a id="5384" href="Data.List.Extrema.html#5345" class="Bound">⊥</a> <a id="5386" href="Data.List.Extrema.html#5347" class="Bound">xs</a> <a id="5389" href="Relation.Binary.Structures.html#2438" class="Function">refl</a>
<a id="5397" href="Data.List.Extrema.html#5397" class="Function">f[argmax]≈f[v]⁺</a> <a id="5413" class="Symbol">:</a> <a id="5415" class="Symbol">∀</a> <a id="5417" class="Symbol">{</a><a id="5418" href="Data.List.Extrema.html#5418" class="Bound">v</a> <a id="5420" href="Data.List.Extrema.html#5420" class="Bound">⊥</a> <a id="5422" href="Data.List.Extrema.html#5422" class="Bound">xs</a><a id="5424" class="Symbol">}</a> <a id="5426" class="Symbol">→</a> <a id="5428" href="Data.List.Extrema.html#5418" class="Bound">v</a> <a id="5430" href="Data.List.Membership.Setoid.html#887" class="Function Operator">∈</a> <a id="5432" href="Data.List.Extrema.html#5422" class="Bound">xs</a> <a id="5435" class="Symbol">→</a> <a id="5437" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="5441" class="Symbol">(λ</a> <a id="5444" href="Data.List.Extrema.html#5444" class="Bound">x</a> <a id="5446" class="Symbol">→</a> <a id="5448" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="5450" href="Data.List.Extrema.html#5444" class="Bound">x</a> <a id="5452" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="5454" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="5456" href="Data.List.Extrema.html#5418" class="Bound">v</a><a id="5457" class="Symbol">)</a> <a id="5459" href="Data.List.Extrema.html#5422" class="Bound">xs</a> <a id="5462" class="Symbol">→</a> <a id="5464" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="5466" href="Data.List.Extrema.html#5420" class="Bound">⊥</a> <a id="5468" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="5470" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="5472" href="Data.List.Extrema.html#5418" class="Bound">v</a> <a id="5474" class="Symbol">→</a>
<a id="5496" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="5498" class="Symbol">(</a><a id="5499" href="Data.List.Extrema.html#1835" class="Function">argmax</a> <a id="5506" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="5508" href="Data.List.Extrema.html#5420" class="Bound">⊥</a> <a id="5510" href="Data.List.Extrema.html#5422" class="Bound">xs</a><a id="5512" class="Symbol">)</a> <a id="5514" href="Relation.Binary.Bundles.html#5573" class="Field Operator">≈</a> <a id="5516" href="Data.List.Extrema.html#4510" class="Bound">f</a> <a id="5518" href="Data.List.Extrema.html#5418" class="Bound">v</a>
<a id="5522" href="Data.List.Extrema.html#5397" class="Function">f[argmax]≈f[v]⁺</a> <a id="5538" href="Data.List.Extrema.html#5538" class="Bound">v∈xs</a> <a id="5543" href="Data.List.Extrema.html#5543" class="Bound">fxs≤fv</a> <a id="5550" href="Data.List.Extrema.html#5550" class="Bound">f⊥≤fv</a> <a id="5556" class="Symbol">=</a> <a id="5558" href="Relation.Binary.Structures.html#3275" class="Function">antisym</a>
<a id="5570" class="Symbol">(</a><a id="5571" href="Data.List.Extrema.html#4846" class="Function">f[argmax]≤v⁺</a> <a id="5584" href="Data.List.Extrema.html#5550" class="Bound">f⊥≤fv</a> <a id="5590" href="Data.List.Extrema.html#5543" class="Bound">fxs≤fv</a><a id="5596" class="Symbol">)</a>
<a id="5602" class="Symbol">(</a><a id="5603" href="Data.List.Extrema.html#4530" class="Function">v≤f[argmax]⁺</a> <a id="5616" class="Symbol">_</a> <a id="5618" class="Symbol">_</a> <a id="5620" class="Symbol">(</a><a id="5621" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="5626" class="Symbol">(</a><a id="5627" href="Data.List.Membership.Propositional.html#1052" class="Function">lose</a> <a id="5632" href="Data.List.Extrema.html#5538" class="Bound">v∈xs</a> <a id="5637" href="Relation.Binary.Structures.html#2438" class="Function">refl</a><a id="5641" class="Symbol">)))</a>
<a id="argmax[xs]≤argmax[ys]⁺"></a><a id="5646" href="Data.List.Extrema.html#5646" class="Function">argmax[xs]≤argmax[ys]⁺</a> <a id="5669" class="Symbol">:</a> <a id="5671" class="Symbol">∀</a> <a id="5673" class="Symbol">{</a><a id="5674" href="Data.List.Extrema.html#5674" class="Bound">f</a> <a id="5676" href="Data.List.Extrema.html#5676" class="Bound">g</a> <a id="5678" class="Symbol">:</a> <a id="5680" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="5682" class="Symbol">→</a> <a id="5684" href="Data.List.Extrema.html#1496" class="Field">B</a><a id="5685" class="Symbol">}</a> <a id="5687" class="Symbol">{</a><a id="5688" href="Data.List.Extrema.html#5688" class="Bound">⊥₁</a><a id="5690" class="Symbol">}</a> <a id="5692" href="Data.List.Extrema.html#5692" class="Bound">⊥₂</a> <a id="5695" class="Symbol">{</a><a id="5696" href="Data.List.Extrema.html#5696" class="Bound">xs</a> <a id="5699" class="Symbol">:</a> <a id="5701" href="Agda.Builtin.List.html#148" class="Datatype">List</a> <a id="5706" href="Data.List.Extrema.html#1668" class="Generalizable">A</a><a id="5707" class="Symbol">}</a> <a id="5709" href="Data.List.Extrema.html#5709" class="Bound">ys</a> <a id="5712" class="Symbol">→</a>
<a id="5739" class="Symbol">(</a><a id="5740" href="Data.List.Extrema.html#5674" class="Bound">f</a> <a id="5742" href="Data.List.Extrema.html#5688" class="Bound">⊥₁</a> <a id="5745" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="5747" href="Data.List.Extrema.html#5676" class="Bound">g</a> <a id="5749" href="Data.List.Extrema.html#5692" class="Bound">⊥₂</a><a id="5751" class="Symbol">)</a> <a id="5753" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="5755" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="5759" class="Symbol">(λ</a> <a id="5762" href="Data.List.Extrema.html#5762" class="Bound">y</a> <a id="5764" class="Symbol">→</a> <a id="5766" href="Data.List.Extrema.html#5674" class="Bound">f</a> <a id="5768" href="Data.List.Extrema.html#5688" class="Bound">⊥₁</a> <a id="5771" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="5773" href="Data.List.Extrema.html#5676" class="Bound">g</a> <a id="5775" href="Data.List.Extrema.html#5762" class="Bound">y</a><a id="5776" class="Symbol">)</a> <a id="5778" href="Data.List.Extrema.html#5709" class="Bound">ys</a> <a id="5781" class="Symbol">→</a>
<a id="5808" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="5812" class="Symbol">(λ</a> <a id="5815" href="Data.List.Extrema.html#5815" class="Bound">x</a> <a id="5817" class="Symbol">→</a> <a id="5819" class="Symbol">(</a><a id="5820" href="Data.List.Extrema.html#5674" class="Bound">f</a> <a id="5822" href="Data.List.Extrema.html#5815" class="Bound">x</a> <a id="5824" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="5826" href="Data.List.Extrema.html#5676" class="Bound">g</a> <a id="5828" href="Data.List.Extrema.html#5692" class="Bound">⊥₂</a><a id="5830" class="Symbol">)</a> <a id="5832" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="5834" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="5838" class="Symbol">(λ</a> <a id="5841" href="Data.List.Extrema.html#5841" class="Bound">y</a> <a id="5843" class="Symbol">→</a> <a id="5845" href="Data.List.Extrema.html#5674" class="Bound">f</a> <a id="5847" href="Data.List.Extrema.html#5815" class="Bound">x</a> <a id="5849" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="5851" href="Data.List.Extrema.html#5676" class="Bound">g</a> <a id="5853" href="Data.List.Extrema.html#5841" class="Bound">y</a><a id="5854" class="Symbol">)</a> <a id="5856" href="Data.List.Extrema.html#5709" class="Bound">ys</a><a id="5858" class="Symbol">)</a> <a id="5860" href="Data.List.Extrema.html#5696" class="Bound">xs</a> <a id="5863" class="Symbol">→</a>
<a id="5890" href="Data.List.Extrema.html#5674" class="Bound">f</a> <a id="5892" class="Symbol">(</a><a id="5893" href="Data.List.Extrema.html#1835" class="Function">argmax</a> <a id="5900" href="Data.List.Extrema.html#5674" class="Bound">f</a> <a id="5902" href="Data.List.Extrema.html#5688" class="Bound">⊥₁</a> <a id="5905" href="Data.List.Extrema.html#5696" class="Bound">xs</a><a id="5907" class="Symbol">)</a> <a id="5909" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="5911" href="Data.List.Extrema.html#5676" class="Bound">g</a> <a id="5913" class="Symbol">(</a><a id="5914" href="Data.List.Extrema.html#1835" class="Function">argmax</a> <a id="5921" href="Data.List.Extrema.html#5676" class="Bound">g</a> <a id="5923" href="Data.List.Extrema.html#5692" class="Bound">⊥₂</a> <a id="5926" href="Data.List.Extrema.html#5709" class="Bound">ys</a><a id="5928" class="Symbol">)</a>
<a id="5930" href="Data.List.Extrema.html#5646" class="Function">argmax[xs]≤argmax[ys]⁺</a> <a id="5953" href="Data.List.Extrema.html#5953" class="Bound">⊥₂</a> <a id="5956" href="Data.List.Extrema.html#5956" class="Bound">ys</a> <a id="5959" href="Data.List.Extrema.html#5959" class="Bound">⊥₁≤ys</a> <a id="5965" href="Data.List.Extrema.html#5965" class="Bound">xs≤ys</a> <a id="5971" class="Symbol">=</a>
<a id="5975" href="Data.List.Extrema.html#4846" class="Function">f[argmax]≤v⁺</a> <a id="5988" class="Symbol">(</a><a id="5989" href="Data.List.Extrema.html#4530" class="Function">v≤f[argmax]⁺</a> <a id="6002" href="Data.List.Extrema.html#5953" class="Bound">⊥₂</a> <a id="6005" class="Symbol">_</a> <a id="6007" href="Data.List.Extrema.html#5959" class="Bound">⊥₁≤ys</a><a id="6012" class="Symbol">)</a> <a id="6014" class="Symbol">(</a><a id="6015" href="Data.List.Relation.Unary.All.html#2935" class="Function">map</a> <a id="6019" class="Symbol">(</a><a id="6020" href="Data.List.Extrema.html#4530" class="Function">v≤f[argmax]⁺</a> <a id="6033" href="Data.List.Extrema.html#5953" class="Bound">⊥₂</a> <a id="6036" href="Data.List.Extrema.html#5956" class="Bound">ys</a><a id="6038" class="Symbol">)</a> <a id="6040" href="Data.List.Extrema.html#5965" class="Bound">xs≤ys</a><a id="6045" class="Symbol">)</a>
<a id="argmax[xs]<argmax[ys]⁺"></a><a id="6048" href="Data.List.Extrema.html#6048" class="Function">argmax[xs]<argmax[ys]⁺</a> <a id="6071" class="Symbol">:</a> <a id="6073" class="Symbol">∀</a> <a id="6075" class="Symbol">{</a><a id="6076" href="Data.List.Extrema.html#6076" class="Bound">f</a> <a id="6078" href="Data.List.Extrema.html#6078" class="Bound">g</a> <a id="6080" class="Symbol">:</a> <a id="6082" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="6084" class="Symbol">→</a> <a id="6086" href="Data.List.Extrema.html#1496" class="Field">B</a><a id="6087" class="Symbol">}</a> <a id="6089" class="Symbol">{</a><a id="6090" href="Data.List.Extrema.html#6090" class="Bound">⊥₁</a><a id="6092" class="Symbol">}</a> <a id="6094" href="Data.List.Extrema.html#6094" class="Bound">⊥₂</a> <a id="6097" class="Symbol">{</a><a id="6098" href="Data.List.Extrema.html#6098" class="Bound">xs</a> <a id="6101" class="Symbol">:</a> <a id="6103" href="Agda.Builtin.List.html#148" class="Datatype">List</a> <a id="6108" href="Data.List.Extrema.html#1668" class="Generalizable">A</a><a id="6109" class="Symbol">}</a> <a id="6111" href="Data.List.Extrema.html#6111" class="Bound">ys</a> <a id="6114" class="Symbol">→</a>
<a id="6141" class="Symbol">(</a><a id="6142" href="Data.List.Extrema.html#6076" class="Bound">f</a> <a id="6144" href="Data.List.Extrema.html#6090" class="Bound">⊥₁</a> <a id="6147" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="6149" href="Data.List.Extrema.html#6078" class="Bound">g</a> <a id="6151" href="Data.List.Extrema.html#6094" class="Bound">⊥₂</a><a id="6153" class="Symbol">)</a> <a id="6155" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="6157" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="6161" class="Symbol">(λ</a> <a id="6164" href="Data.List.Extrema.html#6164" class="Bound">y</a> <a id="6166" class="Symbol">→</a> <a id="6168" href="Data.List.Extrema.html#6076" class="Bound">f</a> <a id="6170" href="Data.List.Extrema.html#6090" class="Bound">⊥₁</a> <a id="6173" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="6175" href="Data.List.Extrema.html#6078" class="Bound">g</a> <a id="6177" href="Data.List.Extrema.html#6164" class="Bound">y</a><a id="6178" class="Symbol">)</a> <a id="6180" href="Data.List.Extrema.html#6111" class="Bound">ys</a> <a id="6183" class="Symbol">→</a>
<a id="6210" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="6214" class="Symbol">(λ</a> <a id="6217" href="Data.List.Extrema.html#6217" class="Bound">x</a> <a id="6219" class="Symbol">→</a> <a id="6221" class="Symbol">(</a><a id="6222" href="Data.List.Extrema.html#6076" class="Bound">f</a> <a id="6224" href="Data.List.Extrema.html#6217" class="Bound">x</a> <a id="6226" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="6228" href="Data.List.Extrema.html#6078" class="Bound">g</a> <a id="6230" href="Data.List.Extrema.html#6094" class="Bound">⊥₂</a><a id="6232" class="Symbol">)</a> <a id="6234" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="6236" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="6240" class="Symbol">(λ</a> <a id="6243" href="Data.List.Extrema.html#6243" class="Bound">y</a> <a id="6245" class="Symbol">→</a> <a id="6247" href="Data.List.Extrema.html#6076" class="Bound">f</a> <a id="6249" href="Data.List.Extrema.html#6217" class="Bound">x</a> <a id="6251" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="6253" href="Data.List.Extrema.html#6078" class="Bound">g</a> <a id="6255" href="Data.List.Extrema.html#6243" class="Bound">y</a><a id="6256" class="Symbol">)</a> <a id="6258" href="Data.List.Extrema.html#6111" class="Bound">ys</a><a id="6260" class="Symbol">)</a> <a id="6262" href="Data.List.Extrema.html#6098" class="Bound">xs</a> <a id="6265" class="Symbol">→</a>
<a id="6292" href="Data.List.Extrema.html#6076" class="Bound">f</a> <a id="6294" class="Symbol">(</a><a id="6295" href="Data.List.Extrema.html#1835" class="Function">argmax</a> <a id="6302" href="Data.List.Extrema.html#6076" class="Bound">f</a> <a id="6304" href="Data.List.Extrema.html#6090" class="Bound">⊥₁</a> <a id="6307" href="Data.List.Extrema.html#6098" class="Bound">xs</a><a id="6309" class="Symbol">)</a> <a id="6311" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="6313" href="Data.List.Extrema.html#6078" class="Bound">g</a> <a id="6315" class="Symbol">(</a><a id="6316" href="Data.List.Extrema.html#1835" class="Function">argmax</a> <a id="6323" href="Data.List.Extrema.html#6078" class="Bound">g</a> <a id="6325" href="Data.List.Extrema.html#6094" class="Bound">⊥₂</a> <a id="6328" href="Data.List.Extrema.html#6111" class="Bound">ys</a><a id="6330" class="Symbol">)</a>
<a id="6332" href="Data.List.Extrema.html#6048" class="Function">argmax[xs]<argmax[ys]⁺</a> <a id="6355" href="Data.List.Extrema.html#6355" class="Bound">⊥₂</a> <a id="6358" href="Data.List.Extrema.html#6358" class="Bound">ys</a> <a id="6361" href="Data.List.Extrema.html#6361" class="Bound">⊥₁<ys</a> <a id="6367" href="Data.List.Extrema.html#6367" class="Bound">xs<ys</a> <a id="6373" class="Symbol">=</a>
<a id="6377" href="Data.List.Extrema.html#5000" class="Function">f[argmax]<v⁺</a> <a id="6390" class="Symbol">(</a><a id="6391" href="Data.List.Extrema.html#4688" class="Function">v<f[argmax]⁺</a> <a id="6404" href="Data.List.Extrema.html#6355" class="Bound">⊥₂</a> <a id="6407" class="Symbol">_</a> <a id="6409" href="Data.List.Extrema.html#6361" class="Bound">⊥₁<ys</a><a id="6414" class="Symbol">)</a> <a id="6416" class="Symbol">(</a><a id="6417" href="Data.List.Relation.Unary.All.html#2935" class="Function">map</a> <a id="6421" class="Symbol">(</a><a id="6422" href="Data.List.Extrema.html#4688" class="Function">v<f[argmax]⁺</a> <a id="6435" href="Data.List.Extrema.html#6355" class="Bound">⊥₂</a> <a id="6438" href="Data.List.Extrema.html#6358" class="Bound">ys</a><a id="6440" class="Symbol">)</a> <a id="6442" href="Data.List.Extrema.html#6367" class="Bound">xs<ys</a><a id="6447" class="Symbol">)</a>
<a id="argmax-sel"></a><a id="6450" href="Data.List.Extrema.html#6450" class="Function">argmax-sel</a> <a id="6461" class="Symbol">:</a> <a id="6463" class="Symbol">∀</a> <a id="6465" class="Symbol">(</a><a id="6466" href="Data.List.Extrema.html#6466" class="Bound">f</a> <a id="6468" class="Symbol">:</a> <a id="6470" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="6472" class="Symbol">→</a> <a id="6474" href="Data.List.Extrema.html#1496" class="Field">B</a><a id="6475" class="Symbol">)</a> <a id="6477" href="Data.List.Extrema.html#6477" class="Bound">⊥</a> <a id="6479" href="Data.List.Extrema.html#6479" class="Bound">xs</a> <a id="6482" class="Symbol">→</a> <a id="6484" class="Symbol">(</a><a id="6485" href="Data.List.Extrema.html#1835" class="Function">argmax</a> <a id="6492" href="Data.List.Extrema.html#6466" class="Bound">f</a> <a id="6494" href="Data.List.Extrema.html#6477" class="Bound">⊥</a> <a id="6496" href="Data.List.Extrema.html#6479" class="Bound">xs</a> <a id="6499" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="6501" href="Data.List.Extrema.html#6477" class="Bound">⊥</a><a id="6502" class="Symbol">)</a> <a id="6504" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="6506" class="Symbol">(</a><a id="6507" href="Data.List.Extrema.html#1835" class="Function">argmax</a> <a id="6514" href="Data.List.Extrema.html#6466" class="Bound">f</a> <a id="6516" href="Data.List.Extrema.html#6477" class="Bound">⊥</a> <a id="6518" href="Data.List.Extrema.html#6479" class="Bound">xs</a> <a id="6521" href="Data.List.Membership.Setoid.html#887" class="Function Operator">∈</a> <a id="6523" href="Data.List.Extrema.html#6479" class="Bound">xs</a><a id="6525" class="Symbol">)</a>
<a id="6527" href="Data.List.Extrema.html#6450" class="Function">argmax-sel</a> <a id="6538" href="Data.List.Extrema.html#6538" class="Bound">f</a> <a id="6540" class="Symbol">=</a> <a id="6542" href="Data.List.Membership.Propositional.Properties.html#11319" class="Function">foldr-selective</a> <a id="6558" class="Symbol">(</a><a id="6559" href="Data.List.Extrema.Core.html#3171" class="Function">⊔ᴸ-sel</a> <a id="6566" href="Data.List.Extrema.html#6538" class="Bound">f</a><a id="6567" class="Symbol">)</a>
<a id="argmax-all"></a><a id="6570" href="Data.List.Extrema.html#6570" class="Function">argmax-all</a> <a id="6581" class="Symbol">:</a> <a id="6583" class="Symbol">∀</a> <a id="6585" class="Symbol">(</a><a id="6586" href="Data.List.Extrema.html#6586" class="Bound">f</a> <a id="6588" class="Symbol">:</a> <a id="6590" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="6592" class="Symbol">→</a> <a id="6594" href="Data.List.Extrema.html#1496" class="Field">B</a><a id="6595" class="Symbol">)</a> <a id="6597" class="Symbol">{</a><a id="6598" href="Data.List.Extrema.html#6598" class="Bound">P</a> <a id="6600" class="Symbol">:</a> <a id="6602" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="6607" href="Data.List.Extrema.html#1668" class="Generalizable">A</a> <a id="6609" href="Data.List.Extrema.html#1654" class="Generalizable">p</a><a id="6610" class="Symbol">}</a> <a id="6612" class="Symbol">{</a><a id="6613" href="Data.List.Extrema.html#6613" class="Bound">⊥</a> <a id="6615" href="Data.List.Extrema.html#6615" class="Bound">xs</a><a id="6617" class="Symbol">}</a> <a id="6619" class="Symbol">→</a>
<a id="6634" href="Data.List.Extrema.html#6598" class="Bound">P</a> <a id="6636" href="Data.List.Extrema.html#6613" class="Bound">⊥</a> <a id="6638" class="Symbol">→</a> <a id="6640" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="6644" href="Data.List.Extrema.html#6598" class="Bound">P</a> <a id="6646" href="Data.List.Extrema.html#6615" class="Bound">xs</a> <a id="6649" class="Symbol">→</a> <a id="6651" href="Data.List.Extrema.html#6598" class="Bound">P</a> <a id="6653" class="Symbol">(</a><a id="6654" href="Data.List.Extrema.html#1835" class="Function">argmax</a> <a id="6661" href="Data.List.Extrema.html#6586" class="Bound">f</a> <a id="6663" href="Data.List.Extrema.html#6613" class="Bound">⊥</a> <a id="6665" href="Data.List.Extrema.html#6615" class="Bound">xs</a><a id="6667" class="Symbol">)</a>
<a id="6669" href="Data.List.Extrema.html#6570" class="Function">argmax-all</a> <a id="6680" href="Data.List.Extrema.html#6680" class="Bound">f</a> <a id="6682" class="Symbol">{</a><a id="6683" class="Argument">P</a> <a id="6685" class="Symbol">=</a> <a id="6687" href="Data.List.Extrema.html#6687" class="Bound">P</a><a id="6688" class="Symbol">}</a> <a id="6690" class="Symbol">{</a><a id="6691" href="Data.List.Extrema.html#6691" class="Bound">⊥</a><a id="6692" class="Symbol">}</a> <a id="6694" class="Symbol">{</a><a id="6695" href="Data.List.Extrema.html#6695" class="Bound">xs</a><a id="6697" class="Symbol">}</a> <a id="6699" href="Data.List.Extrema.html#6699" class="Bound">p⊥</a> <a id="6702" href="Data.List.Extrema.html#6702" class="Bound">pxs</a> <a id="6706" class="Keyword">with</a> <a id="6711" href="Data.List.Extrema.html#6450" class="Function">argmax-sel</a> <a id="6722" href="Data.List.Extrema.html#6680" class="Bound">f</a> <a id="6724" href="Data.List.Extrema.html#6691" class="Bound">⊥</a> <a id="6726" href="Data.List.Extrema.html#6695" class="Bound">xs</a>
<a id="6729" class="Symbol">...</a> <a id="6733" class="Symbol">|</a> <a id="6735" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="6740" href="Data.List.Extrema.html#6740" class="Bound">argmax≡⊥</a> <a id="6750" class="Symbol">=</a> <a id="6752" href="Relation.Binary.PropositionalEquality.Core.html#1780" class="Function">subst</a> <a id="6758" class="Bound">P</a> <a id="6760" class="Symbol">(</a><a id="6761" href="Relation.Binary.PropositionalEquality.Core.html#1684" class="Function">sym</a> <a id="6765" href="Data.List.Extrema.html#6740" class="Bound">argmax≡⊥</a><a id="6773" class="Symbol">)</a> <a id="6775" class="Bound">p⊥</a>
<a id="6778" class="Symbol">...</a> <a id="6782" class="Symbol">|</a> <a id="6784" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="6789" href="Data.List.Extrema.html#6789" class="Bound">argmax∈xs</a> <a id="6799" class="Symbol">=</a> <a id="6801" href="Data.List.Relation.Unary.All.html#5766" class="Function">lookup</a> <a id="6808" class="Bound">pxs</a> <a id="6812" href="Data.List.Extrema.html#6789" class="Bound">argmax∈xs</a>
<a id="6823" class="Comment">------------------------------------------------------------------------------</a>
<a id="6902" class="Comment">-- Properties of min</a>
<a id="min≤v⁺"></a><a id="6924" href="Data.List.Extrema.html#6924" class="Function">min≤v⁺</a> <a id="6931" class="Symbol">:</a> <a id="6933" class="Symbol">∀</a> <a id="6935" class="Symbol">{</a><a id="6936" href="Data.List.Extrema.html#6936" class="Bound">v</a><a id="6937" class="Symbol">}</a> <a id="6939" href="Data.List.Extrema.html#6939" class="Bound">⊤</a> <a id="6941" href="Data.List.Extrema.html#6941" class="Bound">xs</a> <a id="6944" class="Symbol">→</a> <a id="6946" href="Data.List.Extrema.html#6939" class="Bound">⊤</a> <a id="6948" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="6950" href="Data.List.Extrema.html#6936" class="Bound">v</a> <a id="6952" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="6954" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="6958" class="Symbol">(</a><a id="6959" href="Relation.Binary.Bundles.html#5607" class="Field Operator">_≤</a> <a id="6962" href="Data.List.Extrema.html#6936" class="Bound">v</a><a id="6963" class="Symbol">)</a> <a id="6965" href="Data.List.Extrema.html#6941" class="Bound">xs</a> <a id="6968" class="Symbol">→</a> <a id="6970" href="Data.List.Extrema.html#1898" class="Function">min</a> <a id="6974" href="Data.List.Extrema.html#6939" class="Bound">⊤</a> <a id="6976" href="Data.List.Extrema.html#6941" class="Bound">xs</a> <a id="6979" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="6981" href="Data.List.Extrema.html#6936" class="Bound">v</a>
<a id="6983" href="Data.List.Extrema.html#6924" class="Function">min≤v⁺</a> <a id="6990" class="Symbol">=</a> <a id="6992" href="Data.List.Extrema.html#2108" class="Function">f[argmin]≤v⁺</a>
<a id="min<v⁺"></a><a id="7006" href="Data.List.Extrema.html#7006" class="Function">min<v⁺</a> <a id="7013" class="Symbol">:</a> <a id="7015" class="Symbol">∀</a> <a id="7017" class="Symbol">{</a><a id="7018" href="Data.List.Extrema.html#7018" class="Bound">v</a><a id="7019" class="Symbol">}</a> <a id="7021" href="Data.List.Extrema.html#7021" class="Bound">⊤</a> <a id="7023" href="Data.List.Extrema.html#7023" class="Bound">xs</a> <a id="7026" class="Symbol">→</a> <a id="7028" href="Data.List.Extrema.html#7021" class="Bound">⊤</a> <a id="7030" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="7032" href="Data.List.Extrema.html#7018" class="Bound">v</a> <a id="7034" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="7036" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="7040" class="Symbol">(</a><a id="7041" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator">_<</a> <a id="7044" href="Data.List.Extrema.html#7018" class="Bound">v</a><a id="7045" class="Symbol">)</a> <a id="7047" href="Data.List.Extrema.html#7023" class="Bound">xs</a> <a id="7050" class="Symbol">→</a> <a id="7052" href="Data.List.Extrema.html#1898" class="Function">min</a> <a id="7056" href="Data.List.Extrema.html#7021" class="Bound">⊤</a> <a id="7058" href="Data.List.Extrema.html#7023" class="Bound">xs</a> <a id="7061" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="7063" href="Data.List.Extrema.html#7018" class="Bound">v</a>
<a id="7065" href="Data.List.Extrema.html#7006" class="Function">min<v⁺</a> <a id="7072" class="Symbol">=</a> <a id="7074" href="Data.List.Extrema.html#2266" class="Function">f[argmin]<v⁺</a>
<a id="v≤min⁺"></a><a id="7088" href="Data.List.Extrema.html#7088" class="Function">v≤min⁺</a> <a id="7095" class="Symbol">:</a> <a id="7097" class="Symbol">∀</a> <a id="7099" class="Symbol">{</a><a id="7100" href="Data.List.Extrema.html#7100" class="Bound">v</a> <a id="7102" href="Data.List.Extrema.html#7102" class="Bound">⊤</a> <a id="7104" href="Data.List.Extrema.html#7104" class="Bound">xs</a><a id="7106" class="Symbol">}</a> <a id="7108" class="Symbol">→</a> <a id="7110" href="Data.List.Extrema.html#7100" class="Bound">v</a> <a id="7112" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="7114" href="Data.List.Extrema.html#7102" class="Bound">⊤</a> <a id="7116" class="Symbol">→</a> <a id="7118" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="7122" class="Symbol">(</a><a id="7123" href="Data.List.Extrema.html#7100" class="Bound">v</a> <a id="7125" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤_</a><a id="7127" class="Symbol">)</a> <a id="7129" href="Data.List.Extrema.html#7104" class="Bound">xs</a> <a id="7132" class="Symbol">→</a> <a id="7134" href="Data.List.Extrema.html#7100" class="Bound">v</a> <a id="7136" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="7138" href="Data.List.Extrema.html#1898" class="Function">min</a> <a id="7142" href="Data.List.Extrema.html#7102" class="Bound">⊤</a> <a id="7144" href="Data.List.Extrema.html#7104" class="Bound">xs</a>
<a id="7147" href="Data.List.Extrema.html#7088" class="Function">v≤min⁺</a> <a id="7154" class="Symbol">=</a> <a id="7156" href="Data.List.Extrema.html#2424" class="Function">v≤f[argmin]⁺</a>
<a id="v<min⁺"></a><a id="7170" href="Data.List.Extrema.html#7170" class="Function">v<min⁺</a> <a id="7177" class="Symbol">:</a> <a id="7179" class="Symbol">∀</a> <a id="7181" class="Symbol">{</a><a id="7182" href="Data.List.Extrema.html#7182" class="Bound">v</a> <a id="7184" href="Data.List.Extrema.html#7184" class="Bound">⊤</a> <a id="7186" href="Data.List.Extrema.html#7186" class="Bound">xs</a><a id="7188" class="Symbol">}</a> <a id="7190" class="Symbol">→</a> <a id="7192" href="Data.List.Extrema.html#7182" class="Bound">v</a> <a id="7194" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="7196" href="Data.List.Extrema.html#7184" class="Bound">⊤</a> <a id="7198" class="Symbol">→</a> <a id="7200" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="7204" class="Symbol">(</a><a id="7205" href="Data.List.Extrema.html#7182" class="Bound">v</a> <a id="7207" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><_</a><a id="7209" class="Symbol">)</a> <a id="7211" href="Data.List.Extrema.html#7186" class="Bound">xs</a> <a id="7214" class="Symbol">→</a> <a id="7216" href="Data.List.Extrema.html#7182" class="Bound">v</a> <a id="7218" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="7220" href="Data.List.Extrema.html#1898" class="Function">min</a> <a id="7224" href="Data.List.Extrema.html#7184" class="Bound">⊤</a> <a id="7226" href="Data.List.Extrema.html#7186" class="Bound">xs</a>
<a id="7229" href="Data.List.Extrema.html#7170" class="Function">v<min⁺</a> <a id="7236" class="Symbol">=</a> <a id="7238" href="Data.List.Extrema.html#2578" class="Function">v<f[argmin]⁺</a>
<a id="min≤⊤"></a><a id="7252" href="Data.List.Extrema.html#7252" class="Function">min≤⊤</a> <a id="7258" class="Symbol">:</a> <a id="7260" class="Symbol">∀</a> <a id="7262" href="Data.List.Extrema.html#7262" class="Bound">⊤</a> <a id="7264" href="Data.List.Extrema.html#7264" class="Bound">xs</a> <a id="7267" class="Symbol">→</a> <a id="7269" href="Data.List.Extrema.html#1898" class="Function">min</a> <a id="7273" href="Data.List.Extrema.html#7262" class="Bound">⊤</a> <a id="7275" href="Data.List.Extrema.html#7264" class="Bound">xs</a> <a id="7278" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="7280" href="Data.List.Extrema.html#7262" class="Bound">⊤</a>
<a id="7282" href="Data.List.Extrema.html#7252" class="Function">min≤⊤</a> <a id="7288" class="Symbol">=</a> <a id="7290" href="Data.List.Extrema.html#2732" class="Function">f[argmin]≤f[⊤]</a>
<a id="min≤xs"></a><a id="7306" href="Data.List.Extrema.html#7306" class="Function">min≤xs</a> <a id="7313" class="Symbol">:</a> <a id="7315" class="Symbol">∀</a> <a id="7317" href="Data.List.Extrema.html#7317" class="Bound">⊥</a> <a id="7319" href="Data.List.Extrema.html#7319" class="Bound">xs</a> <a id="7322" class="Symbol">→</a> <a id="7324" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="7328" class="Symbol">(</a><a id="7329" href="Data.List.Extrema.html#1898" class="Function">min</a> <a id="7333" href="Data.List.Extrema.html#7317" class="Bound">⊥</a> <a id="7335" href="Data.List.Extrema.html#7319" class="Bound">xs</a> <a id="7338" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤_</a><a id="7340" class="Symbol">)</a> <a id="7342" href="Data.List.Extrema.html#7319" class="Bound">xs</a>
<a id="7345" href="Data.List.Extrema.html#7306" class="Function">min≤xs</a> <a id="7352" class="Symbol">=</a> <a id="7354" href="Data.List.Extrema.html#2839" class="Function">f[argmin]≤f[xs]</a>
<a id="min≈v⁺"></a><a id="7371" href="Data.List.Extrema.html#7371" class="Function">min≈v⁺</a> <a id="7378" class="Symbol">:</a> <a id="7380" class="Symbol">∀</a> <a id="7382" class="Symbol">{</a><a id="7383" href="Data.List.Extrema.html#7383" class="Bound">v</a> <a id="7385" href="Data.List.Extrema.html#7385" class="Bound">⊤</a> <a id="7387" href="Data.List.Extrema.html#7387" class="Bound">xs</a><a id="7389" class="Symbol">}</a> <a id="7391" class="Symbol">→</a> <a id="7393" href="Data.List.Extrema.html#7383" class="Bound">v</a> <a id="7395" href="Data.List.Membership.Setoid.html#887" class="Function Operator">∈</a> <a id="7397" href="Data.List.Extrema.html#7387" class="Bound">xs</a> <a id="7400" class="Symbol">→</a> <a id="7402" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="7406" class="Symbol">(</a><a id="7407" href="Data.List.Extrema.html#7383" class="Bound">v</a> <a id="7409" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤_</a><a id="7411" class="Symbol">)</a> <a id="7413" href="Data.List.Extrema.html#7387" class="Bound">xs</a> <a id="7416" class="Symbol">→</a> <a id="7418" href="Data.List.Extrema.html#7383" class="Bound">v</a> <a id="7420" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="7422" href="Data.List.Extrema.html#7385" class="Bound">⊤</a> <a id="7424" class="Symbol">→</a> <a id="7426" href="Data.List.Extrema.html#1898" class="Function">min</a> <a id="7430" href="Data.List.Extrema.html#7385" class="Bound">⊤</a> <a id="7432" href="Data.List.Extrema.html#7387" class="Bound">xs</a> <a id="7435" href="Relation.Binary.Bundles.html#5573" class="Field Operator">≈</a> <a id="7437" href="Data.List.Extrema.html#7383" class="Bound">v</a>
<a id="7439" href="Data.List.Extrema.html#7371" class="Function">min≈v⁺</a> <a id="7446" class="Symbol">=</a> <a id="7448" href="Data.List.Extrema.html#2975" class="Function">f[argmin]≈f[v]⁺</a>
<a id="min[xs]≤min[ys]⁺"></a><a id="7465" href="Data.List.Extrema.html#7465" class="Function">min[xs]≤min[ys]⁺</a> <a id="7482" class="Symbol">:</a> <a id="7484" class="Symbol">∀</a> <a id="7486" href="Data.List.Extrema.html#7486" class="Bound">⊤₁</a> <a id="7489" class="Symbol">{</a><a id="7490" href="Data.List.Extrema.html#7490" class="Bound">⊤₂</a><a id="7492" class="Symbol">}</a> <a id="7494" href="Data.List.Extrema.html#7494" class="Bound">xs</a> <a id="7497" class="Symbol">{</a><a id="7498" href="Data.List.Extrema.html#7498" class="Bound">ys</a><a id="7500" class="Symbol">}</a> <a id="7502" class="Symbol">→</a> <a id="7504" class="Symbol">(</a><a id="7505" href="Data.List.Extrema.html#7486" class="Bound">⊤₁</a> <a id="7508" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="7510" href="Data.List.Extrema.html#7490" class="Bound">⊤₂</a><a id="7512" class="Symbol">)</a> <a id="7514" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="7516" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="7520" class="Symbol">(</a><a id="7521" href="Relation.Binary.Bundles.html#5607" class="Field Operator">_≤</a> <a id="7524" href="Data.List.Extrema.html#7490" class="Bound">⊤₂</a><a id="7526" class="Symbol">)</a> <a id="7528" href="Data.List.Extrema.html#7494" class="Bound">xs</a> <a id="7531" class="Symbol">→</a>
<a id="7552" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="7556" class="Symbol">(λ</a> <a id="7559" href="Data.List.Extrema.html#7559" class="Bound">y</a> <a id="7561" class="Symbol">→</a> <a id="7563" class="Symbol">(</a><a id="7564" href="Data.List.Extrema.html#7486" class="Bound">⊤₁</a> <a id="7567" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="7569" href="Data.List.Extrema.html#7559" class="Bound">y</a><a id="7570" class="Symbol">)</a> <a id="7572" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="7574" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="7578" class="Symbol">(λ</a> <a id="7581" href="Data.List.Extrema.html#7581" class="Bound">x</a> <a id="7583" class="Symbol">→</a> <a id="7585" href="Data.List.Extrema.html#7581" class="Bound">x</a> <a id="7587" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="7589" href="Data.List.Extrema.html#7559" class="Bound">y</a><a id="7590" class="Symbol">)</a> <a id="7592" href="Data.List.Extrema.html#7494" class="Bound">xs</a><a id="7594" class="Symbol">)</a> <a id="7596" href="Data.List.Extrema.html#7498" class="Bound">ys</a> <a id="7599" class="Symbol">→</a>
<a id="7620" href="Data.List.Extrema.html#1898" class="Function">min</a> <a id="7624" href="Data.List.Extrema.html#7486" class="Bound">⊤₁</a> <a id="7627" href="Data.List.Extrema.html#7494" class="Bound">xs</a> <a id="7630" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="7632" href="Data.List.Extrema.html#1898" class="Function">min</a> <a id="7636" href="Data.List.Extrema.html#7490" class="Bound">⊤₂</a> <a id="7639" href="Data.List.Extrema.html#7498" class="Bound">ys</a>
<a id="7642" href="Data.List.Extrema.html#7465" class="Function">min[xs]≤min[ys]⁺</a> <a id="7659" class="Symbol">=</a> <a id="7661" href="Data.List.Extrema.html#3224" class="Function">argmin[xs]≤argmin[ys]⁺</a>
<a id="min[xs]<min[ys]⁺"></a><a id="7685" href="Data.List.Extrema.html#7685" class="Function">min[xs]<min[ys]⁺</a> <a id="7702" class="Symbol">:</a> <a id="7704" class="Symbol">∀</a> <a id="7706" href="Data.List.Extrema.html#7706" class="Bound">⊤₁</a> <a id="7709" class="Symbol">{</a><a id="7710" href="Data.List.Extrema.html#7710" class="Bound">⊤₂</a><a id="7712" class="Symbol">}</a> <a id="7714" href="Data.List.Extrema.html#7714" class="Bound">xs</a> <a id="7717" class="Symbol">{</a><a id="7718" href="Data.List.Extrema.html#7718" class="Bound">ys</a><a id="7720" class="Symbol">}</a> <a id="7722" class="Symbol">→</a> <a id="7724" class="Symbol">(</a><a id="7725" href="Data.List.Extrema.html#7706" class="Bound">⊤₁</a> <a id="7728" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="7730" href="Data.List.Extrema.html#7710" class="Bound">⊤₂</a><a id="7732" class="Symbol">)</a> <a id="7734" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="7736" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="7740" class="Symbol">(</a><a id="7741" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator">_<</a> <a id="7744" href="Data.List.Extrema.html#7710" class="Bound">⊤₂</a><a id="7746" class="Symbol">)</a> <a id="7748" href="Data.List.Extrema.html#7714" class="Bound">xs</a> <a id="7751" class="Symbol">→</a>
<a id="7772" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="7776" class="Symbol">(λ</a> <a id="7779" href="Data.List.Extrema.html#7779" class="Bound">y</a> <a id="7781" class="Symbol">→</a> <a id="7783" class="Symbol">(</a><a id="7784" href="Data.List.Extrema.html#7706" class="Bound">⊤₁</a> <a id="7787" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="7789" href="Data.List.Extrema.html#7779" class="Bound">y</a><a id="7790" class="Symbol">)</a> <a id="7792" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="7794" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="7798" class="Symbol">(λ</a> <a id="7801" href="Data.List.Extrema.html#7801" class="Bound">x</a> <a id="7803" class="Symbol">→</a> <a id="7805" href="Data.List.Extrema.html#7801" class="Bound">x</a> <a id="7807" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="7809" href="Data.List.Extrema.html#7779" class="Bound">y</a><a id="7810" class="Symbol">)</a> <a id="7812" href="Data.List.Extrema.html#7714" class="Bound">xs</a><a id="7814" class="Symbol">)</a> <a id="7816" href="Data.List.Extrema.html#7718" class="Bound">ys</a> <a id="7819" class="Symbol">→</a>
<a id="7840" href="Data.List.Extrema.html#1898" class="Function">min</a> <a id="7844" href="Data.List.Extrema.html#7706" class="Bound">⊤₁</a> <a id="7847" href="Data.List.Extrema.html#7714" class="Bound">xs</a> <a id="7850" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="7852" href="Data.List.Extrema.html#1898" class="Function">min</a> <a id="7856" href="Data.List.Extrema.html#7710" class="Bound">⊤₂</a> <a id="7859" href="Data.List.Extrema.html#7718" class="Bound">ys</a>
<a id="7862" href="Data.List.Extrema.html#7685" class="Function">min[xs]<min[ys]⁺</a> <a id="7879" class="Symbol">=</a> <a id="7881" href="Data.List.Extrema.html#3623" class="Function">argmin[xs]<argmin[ys]⁺</a>
<a id="min-mono-⊆"></a><a id="7905" href="Data.List.Extrema.html#7905" class="Function">min-mono-⊆</a> <a id="7916" class="Symbol">:</a> <a id="7918" class="Symbol">∀</a> <a id="7920" class="Symbol">{</a><a id="7921" href="Data.List.Extrema.html#7921" class="Bound">⊥₁</a> <a id="7924" href="Data.List.Extrema.html#7924" class="Bound">⊥₂</a> <a id="7927" href="Data.List.Extrema.html#7927" class="Bound">xs</a> <a id="7930" href="Data.List.Extrema.html#7930" class="Bound">ys</a><a id="7932" class="Symbol">}</a> <a id="7934" class="Symbol">→</a> <a id="7936" href="Data.List.Extrema.html#7921" class="Bound">⊥₁</a> <a id="7939" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="7941" href="Data.List.Extrema.html#7924" class="Bound">⊥₂</a> <a id="7944" class="Symbol">→</a> <a id="7946" href="Data.List.Extrema.html#7927" class="Bound">xs</a> <a id="7949" href="Data.List.Relation.Binary.Subset.Setoid.html#801" class="Function Operator">⊇</a> <a id="7951" href="Data.List.Extrema.html#7930" class="Bound">ys</a> <a id="7954" class="Symbol">→</a> <a id="7956" href="Data.List.Extrema.html#1898" class="Function">min</a> <a id="7960" href="Data.List.Extrema.html#7921" class="Bound">⊥₁</a> <a id="7963" href="Data.List.Extrema.html#7927" class="Bound">xs</a> <a id="7966" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="7968" href="Data.List.Extrema.html#1898" class="Function">min</a> <a id="7972" href="Data.List.Extrema.html#7924" class="Bound">⊥₂</a> <a id="7975" href="Data.List.Extrema.html#7930" class="Bound">ys</a>
<a id="7978" href="Data.List.Extrema.html#7905" class="Function">min-mono-⊆</a> <a id="7989" href="Data.List.Extrema.html#7989" class="Bound">⊥₁≤⊥₂</a> <a id="7995" href="Data.List.Extrema.html#7995" class="Bound">ys⊆xs</a> <a id="8001" class="Symbol">=</a> <a id="8003" href="Data.List.Extrema.html#7465" class="Function">min[xs]≤min[ys]⁺</a> <a id="8020" class="Symbol">_</a> <a id="8022" class="Symbol">_</a> <a id="8024" class="Symbol">(</a><a id="8025" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="8030" href="Data.List.Extrema.html#7989" class="Bound">⊥₁≤⊥₂</a><a id="8035" class="Symbol">)</a>
<a id="8039" class="Symbol">(</a><a id="8040" href="Data.List.Relation.Unary.All.html#3725" class="Function">tabulate</a> <a id="8049" class="Symbol">(</a><a id="8050" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="8055" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="8057" href="Data.List.Relation.Unary.Any.html#1643" class="Function">Any.map</a> <a id="8065" class="Symbol">(λ</a> <a id="8068" class="Symbol">{</a><a id="8069" href="Data.List.Extrema.html#1308" class="InductiveConstructor">≡-refl</a> <a id="8076" class="Symbol">→</a> <a id="8078" href="Relation.Binary.Structures.html#2438" class="Function">refl</a><a id="8082" class="Symbol">})</a> <a id="8085" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="8087" href="Data.List.Extrema.html#7995" class="Bound">ys⊆xs</a><a id="8092" class="Symbol">))</a>
<a id="8096" class="Comment">------------------------------------------------------------------------------</a>
<a id="8175" class="Comment">-- Properties of max</a>
<a id="max≤v⁺"></a><a id="8197" href="Data.List.Extrema.html#8197" class="Function">max≤v⁺</a> <a id="8204" class="Symbol">:</a> <a id="8206" class="Symbol">∀</a> <a id="8208" class="Symbol">{</a><a id="8209" href="Data.List.Extrema.html#8209" class="Bound">v</a> <a id="8211" href="Data.List.Extrema.html#8211" class="Bound">⊥</a> <a id="8213" href="Data.List.Extrema.html#8213" class="Bound">xs</a><a id="8215" class="Symbol">}</a> <a id="8217" class="Symbol">→</a> <a id="8219" href="Data.List.Extrema.html#8211" class="Bound">⊥</a> <a id="8221" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="8223" href="Data.List.Extrema.html#8209" class="Bound">v</a> <a id="8225" class="Symbol">→</a> <a id="8227" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="8231" class="Symbol">(</a><a id="8232" href="Relation.Binary.Bundles.html#5607" class="Field Operator">_≤</a> <a id="8235" href="Data.List.Extrema.html#8209" class="Bound">v</a><a id="8236" class="Symbol">)</a> <a id="8238" href="Data.List.Extrema.html#8213" class="Bound">xs</a> <a id="8241" class="Symbol">→</a> <a id="8243" href="Data.List.Extrema.html#1936" class="Function">max</a> <a id="8247" href="Data.List.Extrema.html#8211" class="Bound">⊥</a> <a id="8249" href="Data.List.Extrema.html#8213" class="Bound">xs</a> <a id="8252" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="8254" href="Data.List.Extrema.html#8209" class="Bound">v</a>
<a id="8256" href="Data.List.Extrema.html#8197" class="Function">max≤v⁺</a> <a id="8263" class="Symbol">=</a> <a id="8265" href="Data.List.Extrema.html#4846" class="Function">f[argmax]≤v⁺</a>
<a id="max<v⁺"></a><a id="8279" href="Data.List.Extrema.html#8279" class="Function">max<v⁺</a> <a id="8286" class="Symbol">:</a> <a id="8288" class="Symbol">∀</a> <a id="8290" class="Symbol">{</a><a id="8291" href="Data.List.Extrema.html#8291" class="Bound">v</a> <a id="8293" href="Data.List.Extrema.html#8293" class="Bound">⊥</a> <a id="8295" href="Data.List.Extrema.html#8295" class="Bound">xs</a><a id="8297" class="Symbol">}</a> <a id="8299" class="Symbol">→</a> <a id="8301" href="Data.List.Extrema.html#8293" class="Bound">⊥</a> <a id="8303" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="8305" href="Data.List.Extrema.html#8291" class="Bound">v</a> <a id="8307" class="Symbol">→</a> <a id="8309" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="8313" class="Symbol">(</a><a id="8314" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator">_<</a> <a id="8317" href="Data.List.Extrema.html#8291" class="Bound">v</a><a id="8318" class="Symbol">)</a> <a id="8320" href="Data.List.Extrema.html#8295" class="Bound">xs</a> <a id="8323" class="Symbol">→</a> <a id="8325" href="Data.List.Extrema.html#1936" class="Function">max</a> <a id="8329" href="Data.List.Extrema.html#8293" class="Bound">⊥</a> <a id="8331" href="Data.List.Extrema.html#8295" class="Bound">xs</a> <a id="8334" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="8336" href="Data.List.Extrema.html#8291" class="Bound">v</a>
<a id="8338" href="Data.List.Extrema.html#8279" class="Function">max<v⁺</a> <a id="8345" class="Symbol">=</a> <a id="8347" href="Data.List.Extrema.html#5000" class="Function">f[argmax]<v⁺</a>
<a id="v≤max⁺"></a><a id="8361" href="Data.List.Extrema.html#8361" class="Function">v≤max⁺</a> <a id="8368" class="Symbol">:</a> <a id="8370" class="Symbol">∀</a> <a id="8372" class="Symbol">{</a><a id="8373" href="Data.List.Extrema.html#8373" class="Bound">v</a><a id="8374" class="Symbol">}</a> <a id="8376" href="Data.List.Extrema.html#8376" class="Bound">⊥</a> <a id="8378" href="Data.List.Extrema.html#8378" class="Bound">xs</a> <a id="8381" class="Symbol">→</a> <a id="8383" href="Data.List.Extrema.html#8373" class="Bound">v</a> <a id="8385" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="8387" href="Data.List.Extrema.html#8376" class="Bound">⊥</a> <a id="8389" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="8391" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="8395" class="Symbol">(</a><a id="8396" href="Data.List.Extrema.html#8373" class="Bound">v</a> <a id="8398" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤_</a><a id="8400" class="Symbol">)</a> <a id="8402" href="Data.List.Extrema.html#8378" class="Bound">xs</a> <a id="8405" class="Symbol">→</a> <a id="8407" href="Data.List.Extrema.html#8373" class="Bound">v</a> <a id="8409" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="8411" href="Data.List.Extrema.html#1936" class="Function">max</a> <a id="8415" href="Data.List.Extrema.html#8376" class="Bound">⊥</a> <a id="8417" href="Data.List.Extrema.html#8378" class="Bound">xs</a>
<a id="8420" href="Data.List.Extrema.html#8361" class="Function">v≤max⁺</a> <a id="8427" class="Symbol">=</a> <a id="8429" href="Data.List.Extrema.html#4530" class="Function">v≤f[argmax]⁺</a>
<a id="v<max⁺"></a><a id="8443" href="Data.List.Extrema.html#8443" class="Function">v<max⁺</a> <a id="8450" class="Symbol">:</a> <a id="8452" class="Symbol">∀</a> <a id="8454" class="Symbol">{</a><a id="8455" href="Data.List.Extrema.html#8455" class="Bound">v</a><a id="8456" class="Symbol">}</a> <a id="8458" href="Data.List.Extrema.html#8458" class="Bound">⊥</a> <a id="8460" href="Data.List.Extrema.html#8460" class="Bound">xs</a> <a id="8463" class="Symbol">→</a> <a id="8465" href="Data.List.Extrema.html#8455" class="Bound">v</a> <a id="8467" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="8469" href="Data.List.Extrema.html#8458" class="Bound">⊥</a> <a id="8471" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="8473" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="8477" class="Symbol">(</a><a id="8478" href="Data.List.Extrema.html#8455" class="Bound">v</a> <a id="8480" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><_</a><a id="8482" class="Symbol">)</a> <a id="8484" href="Data.List.Extrema.html#8460" class="Bound">xs</a> <a id="8487" class="Symbol">→</a> <a id="8489" href="Data.List.Extrema.html#8455" class="Bound">v</a> <a id="8491" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="8493" href="Data.List.Extrema.html#1936" class="Function">max</a> <a id="8497" href="Data.List.Extrema.html#8458" class="Bound">⊥</a> <a id="8499" href="Data.List.Extrema.html#8460" class="Bound">xs</a>
<a id="8502" href="Data.List.Extrema.html#8443" class="Function">v<max⁺</a> <a id="8509" class="Symbol">=</a> <a id="8511" href="Data.List.Extrema.html#4688" class="Function">v<f[argmax]⁺</a>
<a id="⊥≤max"></a><a id="8525" href="Data.List.Extrema.html#8525" class="Function">⊥≤max</a> <a id="8531" class="Symbol">:</a> <a id="8533" class="Symbol">∀</a> <a id="8535" href="Data.List.Extrema.html#8535" class="Bound">⊥</a> <a id="8537" href="Data.List.Extrema.html#8537" class="Bound">xs</a> <a id="8540" class="Symbol">→</a> <a id="8542" href="Data.List.Extrema.html#8535" class="Bound">⊥</a> <a id="8544" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="8546" href="Data.List.Extrema.html#1936" class="Function">max</a> <a id="8550" href="Data.List.Extrema.html#8535" class="Bound">⊥</a> <a id="8552" href="Data.List.Extrema.html#8537" class="Bound">xs</a>
<a id="8555" href="Data.List.Extrema.html#8525" class="Function">⊥≤max</a> <a id="8561" class="Symbol">=</a> <a id="8563" href="Data.List.Extrema.html#5154" class="Function">f[⊥]≤f[argmax]</a>
<a id="xs≤max"></a><a id="8579" href="Data.List.Extrema.html#8579" class="Function">xs≤max</a> <a id="8586" class="Symbol">:</a> <a id="8588" class="Symbol">∀</a> <a id="8590" href="Data.List.Extrema.html#8590" class="Bound">⊥</a> <a id="8592" href="Data.List.Extrema.html#8592" class="Bound">xs</a> <a id="8595" class="Symbol">→</a> <a id="8597" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="8601" class="Symbol">(</a><a id="8602" href="Relation.Binary.Bundles.html#5607" class="Field Operator">_≤</a> <a id="8605" href="Data.List.Extrema.html#1936" class="Function">max</a> <a id="8609" href="Data.List.Extrema.html#8590" class="Bound">⊥</a> <a id="8611" href="Data.List.Extrema.html#8592" class="Bound">xs</a><a id="8613" class="Symbol">)</a> <a id="8615" href="Data.List.Extrema.html#8592" class="Bound">xs</a>
<a id="8618" href="Data.List.Extrema.html#8579" class="Function">xs≤max</a> <a id="8625" class="Symbol">=</a> <a id="8627" href="Data.List.Extrema.html#5261" class="Function">f[xs]≤f[argmax]</a>
<a id="max≈v⁺"></a><a id="8644" href="Data.List.Extrema.html#8644" class="Function">max≈v⁺</a> <a id="8651" class="Symbol">:</a> <a id="8653" class="Symbol">∀</a> <a id="8655" class="Symbol">{</a><a id="8656" href="Data.List.Extrema.html#8656" class="Bound">v</a> <a id="8658" href="Data.List.Extrema.html#8658" class="Bound">⊤</a> <a id="8660" href="Data.List.Extrema.html#8660" class="Bound">xs</a><a id="8662" class="Symbol">}</a> <a id="8664" class="Symbol">→</a> <a id="8666" href="Data.List.Extrema.html#8656" class="Bound">v</a> <a id="8668" href="Data.List.Membership.Setoid.html#887" class="Function Operator">∈</a> <a id="8670" href="Data.List.Extrema.html#8660" class="Bound">xs</a> <a id="8673" class="Symbol">→</a> <a id="8675" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="8679" class="Symbol">(</a><a id="8680" href="Relation.Binary.Bundles.html#5607" class="Field Operator">_≤</a> <a id="8683" href="Data.List.Extrema.html#8656" class="Bound">v</a><a id="8684" class="Symbol">)</a> <a id="8686" href="Data.List.Extrema.html#8660" class="Bound">xs</a> <a id="8689" class="Symbol">→</a> <a id="8691" href="Data.List.Extrema.html#8658" class="Bound">⊤</a> <a id="8693" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="8695" href="Data.List.Extrema.html#8656" class="Bound">v</a> <a id="8697" class="Symbol">→</a> <a id="8699" href="Data.List.Extrema.html#1936" class="Function">max</a> <a id="8703" href="Data.List.Extrema.html#8658" class="Bound">⊤</a> <a id="8705" href="Data.List.Extrema.html#8660" class="Bound">xs</a> <a id="8708" href="Relation.Binary.Bundles.html#5573" class="Field Operator">≈</a> <a id="8710" href="Data.List.Extrema.html#8656" class="Bound">v</a>
<a id="8712" href="Data.List.Extrema.html#8644" class="Function">max≈v⁺</a> <a id="8719" class="Symbol">=</a> <a id="8721" href="Data.List.Extrema.html#5397" class="Function">f[argmax]≈f[v]⁺</a>
<a id="max[xs]≤max[ys]⁺"></a><a id="8738" href="Data.List.Extrema.html#8738" class="Function">max[xs]≤max[ys]⁺</a> <a id="8755" class="Symbol">:</a> <a id="8757" class="Symbol">∀</a> <a id="8759" class="Symbol">{</a><a id="8760" href="Data.List.Extrema.html#8760" class="Bound">⊥₁</a><a id="8762" class="Symbol">}</a> <a id="8764" href="Data.List.Extrema.html#8764" class="Bound">⊥₂</a> <a id="8767" class="Symbol">{</a><a id="8768" href="Data.List.Extrema.html#8768" class="Bound">xs</a><a id="8770" class="Symbol">}</a> <a id="8772" href="Data.List.Extrema.html#8772" class="Bound">ys</a> <a id="8775" class="Symbol">→</a> <a id="8777" href="Data.List.Extrema.html#8760" class="Bound">⊥₁</a> <a id="8780" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="8782" href="Data.List.Extrema.html#8764" class="Bound">⊥₂</a> <a id="8785" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="8787" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="8791" class="Symbol">(</a><a id="8792" href="Data.List.Extrema.html#8760" class="Bound">⊥₁</a> <a id="8795" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤_</a><a id="8797" class="Symbol">)</a> <a id="8799" href="Data.List.Extrema.html#8772" class="Bound">ys</a> <a id="8802" class="Symbol">→</a>
<a id="8823" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="8827" class="Symbol">(λ</a> <a id="8830" href="Data.List.Extrema.html#8830" class="Bound">x</a> <a id="8832" class="Symbol">→</a> <a id="8834" href="Data.List.Extrema.html#8830" class="Bound">x</a> <a id="8836" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="8838" href="Data.List.Extrema.html#8764" class="Bound">⊥₂</a> <a id="8841" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="8843" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="8847" class="Symbol">(</a><a id="8848" href="Data.List.Extrema.html#8830" class="Bound">x</a> <a id="8850" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤_</a><a id="8852" class="Symbol">)</a> <a id="8854" href="Data.List.Extrema.html#8772" class="Bound">ys</a><a id="8856" class="Symbol">)</a> <a id="8858" href="Data.List.Extrema.html#8768" class="Bound">xs</a> <a id="8861" class="Symbol">→</a>
<a id="8882" href="Data.List.Extrema.html#1936" class="Function">max</a> <a id="8886" href="Data.List.Extrema.html#8760" class="Bound">⊥₁</a> <a id="8889" href="Data.List.Extrema.html#8768" class="Bound">xs</a> <a id="8892" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="8894" href="Data.List.Extrema.html#1936" class="Function">max</a> <a id="8898" href="Data.List.Extrema.html#8764" class="Bound">⊥₂</a> <a id="8901" href="Data.List.Extrema.html#8772" class="Bound">ys</a>
<a id="8904" href="Data.List.Extrema.html#8738" class="Function">max[xs]≤max[ys]⁺</a> <a id="8921" class="Symbol">=</a> <a id="8923" href="Data.List.Extrema.html#5646" class="Function">argmax[xs]≤argmax[ys]⁺</a>
<a id="max[xs]<max[ys]⁺"></a><a id="8947" href="Data.List.Extrema.html#8947" class="Function">max[xs]<max[ys]⁺</a> <a id="8964" class="Symbol">:</a> <a id="8966" class="Symbol">∀</a> <a id="8968" class="Symbol">{</a><a id="8969" href="Data.List.Extrema.html#8969" class="Bound">⊥₁</a><a id="8971" class="Symbol">}</a> <a id="8973" href="Data.List.Extrema.html#8973" class="Bound">⊥₂</a> <a id="8976" class="Symbol">{</a><a id="8977" href="Data.List.Extrema.html#8977" class="Bound">xs</a><a id="8979" class="Symbol">}</a> <a id="8981" href="Data.List.Extrema.html#8981" class="Bound">ys</a> <a id="8984" class="Symbol">→</a> <a id="8986" href="Data.List.Extrema.html#8969" class="Bound">⊥₁</a> <a id="8989" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="8991" href="Data.List.Extrema.html#8973" class="Bound">⊥₂</a> <a id="8994" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="8996" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="9000" class="Symbol">(</a><a id="9001" href="Data.List.Extrema.html#8969" class="Bound">⊥₁</a> <a id="9004" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><_</a><a id="9006" class="Symbol">)</a> <a id="9008" href="Data.List.Extrema.html#8981" class="Bound">ys</a> <a id="9011" class="Symbol">→</a>
<a id="9032" href="Data.List.Relation.Unary.All.html#1444" class="Datatype">All</a> <a id="9036" class="Symbol">(λ</a> <a id="9039" href="Data.List.Extrema.html#9039" class="Bound">x</a> <a id="9041" class="Symbol">→</a> <a id="9043" href="Data.List.Extrema.html#9039" class="Bound">x</a> <a id="9045" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="9047" href="Data.List.Extrema.html#8973" class="Bound">⊥₂</a> <a id="9050" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="9052" href="Data.List.Relation.Unary.Any.html#1156" class="Datatype">Any</a> <a id="9056" class="Symbol">(</a><a id="9057" href="Data.List.Extrema.html#9039" class="Bound">x</a> <a id="9059" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><_</a><a id="9061" class="Symbol">)</a> <a id="9063" href="Data.List.Extrema.html#8981" class="Bound">ys</a><a id="9065" class="Symbol">)</a> <a id="9067" href="Data.List.Extrema.html#8977" class="Bound">xs</a> <a id="9070" class="Symbol">→</a>
<a id="9091" href="Data.List.Extrema.html#1936" class="Function">max</a> <a id="9095" href="Data.List.Extrema.html#8969" class="Bound">⊥₁</a> <a id="9098" href="Data.List.Extrema.html#8977" class="Bound">xs</a> <a id="9101" href="Relation.Binary.Construct.NonStrictToStrict.html#877" class="Function Operator"><</a> <a id="9103" href="Data.List.Extrema.html#1936" class="Function">max</a> <a id="9107" href="Data.List.Extrema.html#8973" class="Bound">⊥₂</a> <a id="9110" href="Data.List.Extrema.html#8981" class="Bound">ys</a>
<a id="9113" href="Data.List.Extrema.html#8947" class="Function">max[xs]<max[ys]⁺</a> <a id="9130" class="Symbol">=</a> <a id="9132" href="Data.List.Extrema.html#6048" class="Function">argmax[xs]<argmax[ys]⁺</a>
<a id="max-mono-⊆"></a><a id="9156" href="Data.List.Extrema.html#9156" class="Function">max-mono-⊆</a> <a id="9167" class="Symbol">:</a> <a id="9169" class="Symbol">∀</a> <a id="9171" class="Symbol">{</a><a id="9172" href="Data.List.Extrema.html#9172" class="Bound">⊥₁</a> <a id="9175" href="Data.List.Extrema.html#9175" class="Bound">⊥₂</a> <a id="9178" href="Data.List.Extrema.html#9178" class="Bound">xs</a> <a id="9181" href="Data.List.Extrema.html#9181" class="Bound">ys</a><a id="9183" class="Symbol">}</a> <a id="9185" class="Symbol">→</a> <a id="9187" href="Data.List.Extrema.html#9172" class="Bound">⊥₁</a> <a id="9190" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="9192" href="Data.List.Extrema.html#9175" class="Bound">⊥₂</a> <a id="9195" class="Symbol">→</a> <a id="9197" href="Data.List.Extrema.html#9178" class="Bound">xs</a> <a id="9200" href="Data.List.Relation.Binary.Subset.Setoid.html#739" class="Function Operator">⊆</a> <a id="9202" href="Data.List.Extrema.html#9181" class="Bound">ys</a> <a id="9205" class="Symbol">→</a> <a id="9207" href="Data.List.Extrema.html#1936" class="Function">max</a> <a id="9211" href="Data.List.Extrema.html#9172" class="Bound">⊥₁</a> <a id="9214" href="Data.List.Extrema.html#9178" class="Bound">xs</a> <a id="9217" href="Relation.Binary.Bundles.html#5607" class="Field Operator">≤</a> <a id="9219" href="Data.List.Extrema.html#1936" class="Function">max</a> <a id="9223" href="Data.List.Extrema.html#9175" class="Bound">⊥₂</a> <a id="9226" href="Data.List.Extrema.html#9181" class="Bound">ys</a>
<a id="9229" href="Data.List.Extrema.html#9156" class="Function">max-mono-⊆</a> <a id="9240" href="Data.List.Extrema.html#9240" class="Bound">⊥₁≤⊥₂</a> <a id="9246" href="Data.List.Extrema.html#9246" class="Bound">xs⊆ys</a> <a id="9252" class="Symbol">=</a> <a id="9254" href="Data.List.Extrema.html#8738" class="Function">max[xs]≤max[ys]⁺</a> <a id="9271" class="Symbol">_</a> <a id="9273" class="Symbol">_</a> <a id="9275" class="Symbol">(</a><a id="9276" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="9281" href="Data.List.Extrema.html#9240" class="Bound">⊥₁≤⊥₂</a><a id="9286" class="Symbol">)</a>
<a id="9290" class="Symbol">(</a><a id="9291" href="Data.List.Relation.Unary.All.html#3725" class="Function">tabulate</a> <a id="9300" class="Symbol">(</a><a id="9301" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="9306" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="9308" href="Data.List.Relation.Unary.Any.html#1643" class="Function">Any.map</a> <a id="9316" class="Symbol">(λ</a> <a id="9319" class="Symbol">{</a><a id="9320" href="Data.List.Extrema.html#1308" class="InductiveConstructor">≡-refl</a> <a id="9327" class="Symbol">→</a> <a id="9329" href="Relation.Binary.Structures.html#2438" class="Function">refl</a><a id="9333" class="Symbol">})</a> <a id="9336" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="9338" href="Data.List.Extrema.html#9246" class="Bound">xs⊆ys</a><a id="9343" class="Symbol">))</a>
</pre></body></html>