Step | Hyp | Ref
| Expression |
1 | | limsupvaluz2.m |
. . 3
β’ (π β π β β€) |
2 | | limsupvaluz2.z |
. . 3
β’ π =
(β€β₯βπ) |
3 | | limsupvaluz2.f |
. . . 4
β’ (π β πΉ:πβΆβ) |
4 | 3 | frexr 44395 |
. . 3
β’ (π β πΉ:πβΆβ*) |
5 | 1, 2, 4 | limsupvaluz 44724 |
. 2
β’ (π β (lim supβπΉ) = inf(ran (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)), β*, < )) |
6 | 3 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ π β π) β πΉ:πβΆβ) |
7 | | id 22 |
. . . . . . . . . . 11
β’ (π β π β π β π) |
8 | 2, 7 | uzssd2 44427 |
. . . . . . . . . 10
β’ (π β π β (β€β₯βπ) β π) |
9 | 8 | adantl 481 |
. . . . . . . . 9
β’ ((π β§ π β π) β (β€β₯βπ) β π) |
10 | 6, 9 | feqresmpt 6962 |
. . . . . . . 8
β’ ((π β§ π β π) β (πΉ βΎ (β€β₯βπ)) = (π β (β€β₯βπ) β¦ (πΉβπ))) |
11 | 10 | rneqd 5938 |
. . . . . . 7
β’ ((π β§ π β π) β ran (πΉ βΎ (β€β₯βπ)) = ran (π β (β€β₯βπ) β¦ (πΉβπ))) |
12 | 11 | supeq1d 9444 |
. . . . . 6
β’ ((π β§ π β π) β sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
= sup(ran (π β
(β€β₯βπ) β¦ (πΉβπ)), β*, <
)) |
13 | | nfcv 2902 |
. . . . . . . . . 10
β’
β²ππΉ |
14 | | limsupvaluz2.r |
. . . . . . . . . . 11
β’ (π β (lim supβπΉ) β
β) |
15 | 14 | renepnfd 11270 |
. . . . . . . . . 10
β’ (π β (lim supβπΉ) β
+β) |
16 | 13, 2, 3, 15 | limsupubuz 44729 |
. . . . . . . . 9
β’ (π β βπ₯ β β βπ β π (πΉβπ) β€ π₯) |
17 | 16 | adantr 480 |
. . . . . . . 8
β’ ((π β§ π β π) β βπ₯ β β βπ β π (πΉβπ) β€ π₯) |
18 | | ssralv 4051 |
. . . . . . . . . . 11
β’
((β€β₯βπ) β π β (βπ β π (πΉβπ) β€ π₯ β βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
19 | 8, 18 | syl 17 |
. . . . . . . . . 10
β’ (π β π β (βπ β π (πΉβπ) β€ π₯ β βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
20 | 19 | adantl 481 |
. . . . . . . . 9
β’ ((π β§ π β π) β (βπ β π (πΉβπ) β€ π₯ β βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
21 | 20 | reximdv 3169 |
. . . . . . . 8
β’ ((π β§ π β π) β (βπ₯ β β βπ β π (πΉβπ) β€ π₯ β βπ₯ β β βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
22 | 17, 21 | mpd 15 |
. . . . . . 7
β’ ((π β§ π β π) β βπ₯ β β βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
23 | | nfv 1916 |
. . . . . . . 8
β’
β²π(π β§ π β π) |
24 | 2 | eluzelz2 44413 |
. . . . . . . . . 10
β’ (π β π β π β β€) |
25 | | uzid 12842 |
. . . . . . . . . 10
β’ (π β β€ β π β
(β€β₯βπ)) |
26 | | ne0i 4335 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β (β€β₯βπ) β β
) |
27 | 24, 25, 26 | 3syl 18 |
. . . . . . . . 9
β’ (π β π β (β€β₯βπ) β β
) |
28 | 27 | adantl 481 |
. . . . . . . 8
β’ ((π β§ π β π) β (β€β₯βπ) β β
) |
29 | 6 | adantr 480 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β πΉ:πβΆβ) |
30 | 9 | sselda 3983 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
31 | 29, 30 | ffvelcdmd 7088 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
32 | 23, 28, 31 | supxrre3rnmpt 44439 |
. . . . . . 7
β’ ((π β§ π β π) β (sup(ran (π β (β€β₯βπ) β¦ (πΉβπ)), β*, < ) β
β β βπ₯
β β βπ
β (β€β₯βπ)(πΉβπ) β€ π₯)) |
33 | 22, 32 | mpbird 256 |
. . . . . 6
β’ ((π β§ π β π) β sup(ran (π β (β€β₯βπ) β¦ (πΉβπ)), β*, < ) β
β) |
34 | 12, 33 | eqeltrd 2832 |
. . . . 5
β’ ((π β§ π β π) β sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
β β) |
35 | 34 | fmpttd 7117 |
. . . 4
β’ (π β (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)):πβΆβ) |
36 | 35 | frnd 6726 |
. . 3
β’ (π β ran (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, < ))
β β) |
37 | | nfv 1916 |
. . . 4
β’
β²ππ |
38 | | eqid 2731 |
. . . 4
β’ (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, < ))
= (π β π β¦ sup(ran (πΉ βΎ
(β€β₯βπ)), β*, <
)) |
39 | 1, 2 | uzn0d 44435 |
. . . 4
β’ (π β π β β
) |
40 | 37, 34, 38, 39 | rnmptn0 6244 |
. . 3
β’ (π β ran (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, < ))
β β
) |
41 | | nfcv 2902 |
. . . . . . . . . 10
β’
β²ππΉ |
42 | 41, 1, 2, 4 | limsupre3uz 44752 |
. . . . . . . . 9
β’ (π β ((lim supβπΉ) β β β
(βπ₯ β β
βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯))) |
43 | 14, 42 | mpbid 231 |
. . . . . . . 8
β’ (π β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
44 | 43 | simpld 494 |
. . . . . . 7
β’ (π β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) |
45 | | simp-4r 781 |
. . . . . . . . . . . 12
β’
(((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ β€ (πΉβπ)) β π₯ β β) |
46 | 45 | rexrd 11269 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ β€ (πΉβπ)) β π₯ β β*) |
47 | 4 | 3ad2ant1 1132 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β πΉ:πβΆβ*) |
48 | 2 | uztrn2 12846 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
49 | 48 | 3adant1 1129 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β π β π) |
50 | 47, 49 | ffvelcdmd 7088 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β (πΉβπ) β
β*) |
51 | 50 | ad5ant134 1366 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ β€ (πΉβπ)) β (πΉβπ) β
β*) |
52 | | rnresss 6018 |
. . . . . . . . . . . . . . . 16
β’ ran
(πΉ βΎ
(β€β₯βπ)) β ran πΉ |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β ran (πΉ βΎ (β€β₯βπ)) β ran πΉ) |
54 | 3 | frnd 6726 |
. . . . . . . . . . . . . . . 16
β’ (π β ran πΉ β β) |
55 | 54 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β ran πΉ β β) |
56 | 53, 55 | sstrd 3993 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β ran (πΉ βΎ (β€β₯βπ)) β
β) |
57 | | ressxr 11263 |
. . . . . . . . . . . . . . 15
β’ β
β β* |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β β β
β*) |
59 | 56, 58 | sstrd 3993 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β ran (πΉ βΎ (β€β₯βπ)) β
β*) |
60 | 59 | supxrcld 44099 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
β β*) |
61 | 60 | ad5ant13 754 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ β€ (πΉβπ)) β sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
β β*) |
62 | | simpr 484 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ β€ (πΉβπ)) β π₯ β€ (πΉβπ)) |
63 | 59 | 3adant3 1131 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β ran (πΉ βΎ (β€β₯βπ)) β
β*) |
64 | | fvres 6911 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯βπ) β ((πΉ βΎ (β€β₯βπ))βπ) = (πΉβπ)) |
65 | 64 | eqcomd 2737 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯βπ) β (πΉβπ) = ((πΉ βΎ (β€β₯βπ))βπ)) |
66 | 65 | 3ad2ant3 1134 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β (πΉβπ) = ((πΉ βΎ (β€β₯βπ))βπ)) |
67 | 3 | ffnd 6719 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΉ Fn π) |
68 | 67 | adantr 480 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β πΉ Fn π) |
69 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β π β π) |
70 | 2, 69 | uzssd2 44427 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β (β€β₯βπ) β π) |
71 | 70 | adantl 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β (β€β₯βπ) β π) |
72 | | fnssres 6674 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ Fn π β§ (β€β₯βπ) β π) β (πΉ βΎ (β€β₯βπ)) Fn
(β€β₯βπ)) |
73 | 68, 71, 72 | syl2anc 583 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β (πΉ βΎ (β€β₯βπ)) Fn
(β€β₯βπ)) |
74 | 73 | 3adant3 1131 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β (πΉ βΎ (β€β₯βπ)) Fn
(β€β₯βπ)) |
75 | | simp3 1137 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
76 | | fnfvelrn 7083 |
. . . . . . . . . . . . . . 15
β’ (((πΉ βΎ
(β€β₯βπ)) Fn (β€β₯βπ) β§ π β (β€β₯βπ)) β ((πΉ βΎ (β€β₯βπ))βπ) β ran (πΉ βΎ (β€β₯βπ))) |
77 | 74, 75, 76 | syl2anc 583 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β ((πΉ βΎ (β€β₯βπ))βπ) β ran (πΉ βΎ (β€β₯βπ))) |
78 | 66, 77 | eqeltrd 2832 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β (πΉβπ) β ran (πΉ βΎ (β€β₯βπ))) |
79 | | eqid 2731 |
. . . . . . . . . . . . 13
β’ sup(ran
(πΉ βΎ
(β€β₯βπ)), β*, < ) = sup(ran
(πΉ βΎ
(β€β₯βπ)), β*, <
) |
80 | 63, 78, 79 | supxrubd 44105 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β (πΉβπ) β€ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)) |
81 | 80 | ad5ant134 1366 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ β€ (πΉβπ)) β (πΉβπ) β€ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)) |
82 | 46, 51, 61, 62, 81 | xrletrd 13146 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ π₯ β€ (πΉβπ)) β π₯ β€ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)) |
83 | 82 | rexlimdva2 3156 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ π β π) β (βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β π₯ β€ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
))) |
84 | 83 | ralimdva 3166 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ β π π₯ β€ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
))) |
85 | 84 | reximdva 3167 |
. . . . . . 7
β’ (π β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ₯ β β βπ β π π₯ β€ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
))) |
86 | 44, 85 | mpd 15 |
. . . . . 6
β’ (π β βπ₯ β β βπ β π π₯ β€ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)) |
87 | 86 | idi 1 |
. . . . 5
β’ (π β βπ₯ β β βπ β π π₯ β€ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)) |
88 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
89 | 88 | reseq2d 5982 |
. . . . . . . . . . 11
β’ (π = π β (πΉ βΎ (β€β₯βπ)) = (πΉ βΎ (β€β₯βπ))) |
90 | 89 | rneqd 5938 |
. . . . . . . . . 10
β’ (π = π β ran (πΉ βΎ (β€β₯βπ)) = ran (πΉ βΎ (β€β₯βπ))) |
91 | 90 | supeq1d 9444 |
. . . . . . . . 9
β’ (π = π β sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
= sup(ran (πΉ βΎ
(β€β₯βπ)), β*, <
)) |
92 | | eqcom 2738 |
. . . . . . . . . . 11
β’ (π = π β π = π) |
93 | 92 | imbi1i 348 |
. . . . . . . . . 10
β’ ((π = π β sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
= sup(ran (πΉ βΎ
(β€β₯βπ)), β*, < )) β
(π = π β sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
= sup(ran (πΉ βΎ
(β€β₯βπ)), β*, <
))) |
94 | | eqcom 2738 |
. . . . . . . . . . 11
β’ (sup(ran
(πΉ βΎ
(β€β₯βπ)), β*, < ) = sup(ran
(πΉ βΎ
(β€β₯βπ)), β*, < ) β
sup(ran (πΉ βΎ
(β€β₯βπ)), β*, < ) = sup(ran
(πΉ βΎ
(β€β₯βπ)), β*, <
)) |
95 | 94 | imbi2i 335 |
. . . . . . . . . 10
β’ ((π = π β sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
= sup(ran (πΉ βΎ
(β€β₯βπ)), β*, < )) β
(π = π β sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
= sup(ran (πΉ βΎ
(β€β₯βπ)), β*, <
))) |
96 | 93, 95 | bitri 274 |
. . . . . . . . 9
β’ ((π = π β sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
= sup(ran (πΉ βΎ
(β€β₯βπ)), β*, < )) β
(π = π β sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
= sup(ran (πΉ βΎ
(β€β₯βπ)), β*, <
))) |
97 | 91, 96 | mpbi 229 |
. . . . . . . 8
β’ (π = π β sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
= sup(ran (πΉ βΎ
(β€β₯βπ)), β*, <
)) |
98 | 97 | breq2d 5161 |
. . . . . . 7
β’ (π = π β (π₯ β€ sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
β π₯ β€ sup(ran
(πΉ βΎ
(β€β₯βπ)), β*, <
))) |
99 | 98 | cbvralvw 3233 |
. . . . . 6
β’
(βπ β
π π₯ β€ sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
β βπ β
π π₯ β€ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)) |
100 | 99 | rexbii 3093 |
. . . . 5
β’
(βπ₯ β
β βπ β
π π₯ β€ sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
β βπ₯ β
β βπ β
π π₯ β€ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)) |
101 | 87, 100 | sylib 217 |
. . . 4
β’ (π β βπ₯ β β βπ β π π₯ β€ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)) |
102 | 34 | elexd 3494 |
. . . . 5
β’ ((π β§ π β π) β sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
β V) |
103 | 37, 102 | rnmptbd2 44253 |
. . . 4
β’ (π β (βπ₯ β β βπ β π π₯ β€ sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
β βπ₯ β
β βπ¦ β
ran (π β π β¦ sup(ran (πΉ βΎ
(β€β₯βπ)), β*, < ))π₯ β€ π¦)) |
104 | 101, 103 | mpbid 231 |
. . 3
β’ (π β βπ₯ β β βπ¦ β ran (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
))π₯ β€ π¦) |
105 | | infxrre 13320 |
. . 3
β’ ((ran
(π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, < ))
β β β§ ran (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, < ))
β β
β§ βπ₯
β β βπ¦
β ran (π β π β¦ sup(ran (πΉ βΎ
(β€β₯βπ)), β*, < ))π₯ β€ π¦) β inf(ran (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)), β*, < ) = inf(ran (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)), β, < )) |
106 | 36, 40, 104, 105 | syl3anc 1370 |
. 2
β’ (π β inf(ran (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)), β*, < ) = inf(ran (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)), β, < )) |
107 | | fveq2 6892 |
. . . . . . . . 9
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
108 | 107 | reseq2d 5982 |
. . . . . . . 8
β’ (π = π β (πΉ βΎ (β€β₯βπ)) = (πΉ βΎ (β€β₯βπ))) |
109 | 108 | rneqd 5938 |
. . . . . . 7
β’ (π = π β ran (πΉ βΎ (β€β₯βπ)) = ran (πΉ βΎ (β€β₯βπ))) |
110 | 109 | supeq1d 9444 |
. . . . . 6
β’ (π = π β sup(ran (πΉ βΎ (β€β₯βπ)), β*, < )
= sup(ran (πΉ βΎ
(β€β₯βπ)), β*, <
)) |
111 | 110 | cbvmptv 5262 |
. . . . 5
β’ (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, < ))
= (π β π β¦ sup(ran (πΉ βΎ
(β€β₯βπ)), β*, <
)) |
112 | 111 | rneqi 5937 |
. . . 4
β’ ran
(π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, < ))
= ran (π β π β¦ sup(ran (πΉ βΎ
(β€β₯βπ)), β*, <
)) |
113 | 112 | infeq1i 9476 |
. . 3
β’ inf(ran
(π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)), β, < ) = inf(ran (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)), β, < ) |
114 | 113 | a1i 11 |
. 2
β’ (π β inf(ran (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)), β, < ) = inf(ran (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)), β, < )) |
115 | 5, 106, 114 | 3eqtrd 2775 |
1
β’ (π β (lim supβπΉ) = inf(ran (π β π β¦ sup(ran (πΉ βΎ (β€β₯βπ)), β*, <
)), β, < )) |