Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cnext Structured version   Visualization version   Unicode version

Definition df-cnext 21153
 Description: Define the continuous extension of a given function. (Contributed by Thierry Arnoux, 1-Dec-2017.)
Assertion
Ref Expression
df-cnext CnExt t
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-cnext
StepHypRef Expression
1 ccnext 21152 . 2 CnExt
2 vj . . 3
3 vk . . 3
4 ctop 19994 . . 3
5 vf . . . 4
63cv 1451 . . . . . 6
76cuni 4190 . . . . 5
82cv 1451 . . . . . 6
98cuni 4190 . . . . 5
10 cpm 7491 . . . . 5
117, 9, 10co 6308 . . . 4
12 vx . . . . 5
135cv 1451 . . . . . . 7
1413cdm 4839 . . . . . 6
15 ccl 20110 . . . . . . 7
168, 15cfv 5589 . . . . . 6
1714, 16cfv 5589 . . . . 5
1812cv 1451 . . . . . . 7
1918csn 3959 . . . . . 6
20 cnei 20190 . . . . . . . . . . 11
218, 20cfv 5589 . . . . . . . . . 10
2219, 21cfv 5589 . . . . . . . . 9
23 crest 15397 . . . . . . . . 9 t
2422, 14, 23co 6308 . . . . . . . 8 t
25 cflf 21028 . . . . . . . 8
266, 24, 25co 6308 . . . . . . 7 t
2713, 26cfv 5589 . . . . . 6 t
2819, 27cxp 4837 . . . . 5 t
2912, 17, 28ciun 4269 . . . 4 t
305, 11, 29cmpt 4454 . . 3 t
312, 3, 4, 4, 30cmpt2 6310 . 2 t
321, 31wceq 1452 1 CnExt t
 Colors of variables: wff setvar class This definition is referenced by:  cnextval  21154
 Copyright terms: Public domain W3C validator