ruc-ai4math/LeanStateSearch2025.3
187
1{2 "version": "1.0",3 "truncation": null,4 "padding": null,5 "added_tokens": [6 {7 "id": 0,8 "content": "[CLS]",9 "single_word": false,10 "lstrip": false,11 "rstrip": false,12 "normalized": false,13 "special": true14 },15 {16 "id": 1,17 "content": "[SEP]",18 "single_word": false,19 "lstrip": false,20 "rstrip": false,21 "normalized": false,22 "special": true23 },24 {25 "id": 2,26 "content": "[PAD]",27 "single_word": false,28 "lstrip": false,29 "rstrip": false,30 "normalized": false,31 "special": true32 },33 {34 "id": 3,35 "content": "[UNK]",36 "single_word": false,37 "lstrip": false,38 "rstrip": false,39 "normalized": false,40 "special": true41 },42 {43 "id": 4,44 "content": "<VAR>",45 "single_word": false,46 "lstrip": false,47 "rstrip": false,48 "normalized": true,49 "special": false50 },51 {52 "id": 5,53 "content": "<GOAL>",54 "single_word": false,55 "lstrip": false,56 "rstrip": false,57 "normalized": true,58 "special": false59 },60 {61 "id": 30520,62 "content": "[MASK]",63 "single_word": false,64 "lstrip": false,65 "rstrip": false,66 "normalized": false,67 "special": true68 }69 ],70 "normalizer": {71 "type": "BertNormalizer",72 "clean_text": true,73 "handle_chinese_chars": true,74 "strip_accents": null,75 "lowercase": false76 },77 "pre_tokenizer": {78 "type": "BertPreTokenizer"79 },80 "post_processor": {81 "type": "TemplateProcessing",82 "single": [83 {84 "SpecialToken": {85 "id": "[CLS]",86 "type_id": 087 }88 },89 {90 "Sequence": {91 "id": "A",92 "type_id": 093 }94 },95 {96 "SpecialToken": {97 "id": "[SEP]",98 "type_id": 099 }100 }101 ],102 "pair": [103 {104 "SpecialToken": {105 "id": "[CLS]",106 "type_id": 0107 }108 },109 {110 "Sequence": {111 "id": "A",112 "type_id": 0113 }114 },115 {116 "SpecialToken": {117 "id": "[SEP]",118 "type_id": 0119 }120 },121 {122 "Sequence": {123 "id": "B",124 "type_id": 1125 }126 },127 {128 "SpecialToken": {129 "id": "[SEP]",130 "type_id": 1131 }132 }133 ],134 "special_tokens": {135 "[CLS]": {136 "id": "[CLS]",137 "ids": [138 0139 ],140 "tokens": [141 "[CLS]"142 ]143 },144 "[SEP]": {145 "id": "[SEP]",146 "ids": [147 1148 ],149 "tokens": [150 "[SEP]"151 ]152 }153 }154 },155 "decoder": {156 "type": "WordPiece",157 "prefix": "##",158 "cleanup": true159 },160 "model": {161 "type": "WordPiece",162 "unk_token": "[UNK]",163 "continuing_subword_prefix": "##",164 "max_input_chars_per_word": 100,165 "vocab": {166 "[CLS]": 0,167 "[SEP]": 1,168 "[PAD]": 2,169 "[UNK]": 3,170 "<VAR>": 4,171 "<GOAL>": 5,172 "!": 6,173 "\"": 7,174 "#": 8,175 "$": 9,176 "%": 10,177 "&": 11,178 "'": 12,179 "(": 13,180 ")": 14,181 "*": 15,182 "+": 16,183 ",": 17,184 "-": 18,185 ".": 19,186 "/": 20,187 "0": 21,188 "1": 22,189 "2": 23,190 "3": 24,191 "4": 25,192 "5": 26,193 "6": 27,194 "7": 28,195 "8": 29,196 "9": 30,197 ":": 31,198 ";": 32,199 "<": 33,200 "=": 34,201 ">": 35,202 "?": 36,203 "@": 37,204 "A": 38,205 "B": 39,206 "C": 40,207 "D": 41,208 "E": 42,209 "F": 43,210 "G": 44,211 "H": 45,212 "I": 46,213 "J": 47,214 "K": 48,215 "L": 49,216 "M": 50,217 "N": 51,218 "O": 52,219 "P": 53,220 "Q": 54,221 "R": 55,222 "S": 56,223 "T": 57,224 "U": 58,225 "V": 59,226 "W": 60,227 "X": 61,228 "Y": 62,229 "Z": 63,230 "[": 64,231 "\\": 65,232 "]": 66,233 "^": 67,234 "_": 68,235 "a": 69,236 "b": 70,237 "c": 71,238 "d": 72,239 "e": 73,240 "f": 74,241 "g": 75,242 "h": 76,243 "i": 77,244 "j": 78,245 "k": 79,246 "l": 80,247 "m": 81,248 "n": 82,249 "o": 83,250 "p": 84,251 "q": 85,252 "r": 86,253 "s": 87,254 "t": 88,255 "u": 89,256 "v": 90,257 "w": 91,258 "x": 92,259 "y": 93,260 "z": 94,261 "{": 95,262 "|": 96,263 "}": 97,264 "~": 98,265 "«": 99,266 "¬": 100,267 "²": 101,268 "³": 102,269 "¹": 103,270 "»": 104,271 "×": 105,272 "ʷ": 106,273 "ʸ": 107,274 "ˢ": 108,275 "ˣ": 109,276 "̂": 110,277 "Γ": 111,278 "Δ": 112,279 "Θ": 113,280 "Ι": 114,281 "Λ": 115,282 "Π": 116,283 "Σ": 117,284 "Φ": 118,285 "Ψ": 119,286 "Ω": 120,287 "α": 121,288 "β": 122,289 "γ": 123,290 "δ": 124,291 "ε": 125,292 "ζ": 126,293 "η": 127,294 "θ": 128,295 "ι": 129,296 "κ": 130,297 "λ": 131,298 "μ": 132,299 "ν": 133,300 "ξ": 134,301 "π": 135,302 "ρ": 136,303 "σ": 137,304 "τ": 138,305 "υ": 139,306 "φ": 140,307 "χ": 141,308 "ψ": 142,309 "ω": 143,310 "ϕ": 144,311 "ϖ": 145,312 "ᗮ": 146,313 "ᘁ": 147,314 "ᴬ": 148,315 "ᴴ": 149,316 "ᴸ": 150,317 "ᴹ": 151,318 "ᵀ": 152,319 "ᵁ": 153,320 "ᵃ": 154,321 "ᵇ": 155,322 "ᵈ": 156,323 "ᵍ": 157,324 "ᵐ": 158,325 "ᵒ": 159,326 "ᵖ": 160,327 "ᵛ": 161,328 "ᵢ": 162,329 "ᵣ": 163,330 "ᵤ": 164,331 "ᵥ": 165,332 "ᶜ": 166,333 "ᶠ": 167,334 "‖": 168,335 "†": 169,336 "•": 170,337 "′": 171,338 "‼": 172,339 "⁄": 173,340 "⁅": 174,341 "⁆": 175,342 "⁰": 176,343 "ⁱ": 177,344 "⁴": 178,345 "⁵": 179,346 "⁶": 180,347 "⁷": 181,348 "⁸": 182,349 "⁹": 183,350 "⁺": 184,351 "⁻": 185,352 "₀": 186,353 "₁": 187,354 "₂": 188,355 "₃": 189,356 "₄": 190,357 "₅": 191,358 "₆": 192,359 "₇": 193,360 "₈": 194,361 "₉": 195,362 "₊": 196,363 "ₐ": 197,364 "ₑ": 198,365 "ₒ": 199,366 "ₕ": 200,367 "ₖ": 201,368 "ₗ": 202,369 "ₘ": 203,370 "ₙ": 204,371 "ₚ": 205,372 "ₛ": 206,373 "ₜ": 207,374 "ℂ": 208,375 "ℋ": 209,376 "ℍ": 210,377 "ℐ": 211,378 "ℑ": 212,379 "ℒ": 213,380 "ℓ": 214,381 "ℕ": 215,382 "ℙ": 216,383 "ℚ": 217,384 "ℜ": 218,385 "ℝ": 219,386 "ℤ": 220,387 "ℬ": 221,388 "ℰ": 222,389 "ℱ": 223,390 "ℳ": 224,391 "ℵ": 225,392 "⅟": 226,393 "←": 227,394 "↑": 228,395 "→": 229,396 "↓": 230,397 "↔": 231,398 "↥": 232,399 "↦": 233,400 "↪": 234,401 "↾": 235,402 "↿": 236,403 "⇑": 237,404 "⇒": 238,405 "⇔": 239,406 "⇨": 240,407 "∀": 241,408 "∂": 242,409 "∃": 243,410 "∅": 244,411 "∆": 245,412 "∇": 246,413 "∈": 247,414 "∉": 248,415 "∏": 249,416 "∐": 250,417 "∑": 251,418 "∗": 252,419 "∘": 253,420 "√": 254,421 "∞": 255,422 "∠": 256,423 "∡": 257,424 "∣": 258,425 "∥": 259,426 "∧": 260,427 "∨": 261,428 "∩": 262,429 "∪": 263,430 "∫": 264,431 "∮": 265,432 "∯": 266,433 "∼": 267,434 "≃": 268,435 "≅": 269,436 "≈": 270,437 "≌": 271,438 "≠": 272,439 "≡": 273,440 "≤": 274,441 "≥": 275,442 "≪": 276,443 "≫": 277,444 "≺": 278,445 "≼": 279,446 "⊂": 280,447 "⊆": 281,448 "⊇": 282,449 "⊓": 283,450 "⊔": 284,451 "⊕": 285,452 "⊗": 286,453 "⊙": 287,454 "⊚": 288,455 "⊛": 289,456 "⊞": 290,457 "⊣": 291,458 "⊤": 292,459 "⊥": 293,460 "⊨": 294,461 "⊻": 295,462 "⊼": 296,463 "⋀": 297,464 "⋂": 298,465 "⋃": 299,466 "⋆": 300,467 "⋈": 301,468 "⋊": 302,469 "⋖": 303,470 "⋙": 304,471 "⋯": 305,472 "⌈": 306,473 "⌉": 307,474 "⌊": 308,475 "⌋": 309,476 "⍟": 310,477 "□": 311,478 "▷": 312,479 "▸": 313,480 "◁": 314,481 "◃": 315,482 "○": 316,483 "◫": 317,484 "♯": 318,485 "✝": 319,486 "✶": 320,487 "⟂": 321,488 "⟦": 322,489 "⟧": 323,490 "⟨": 324,491 "⟩": 325,492 "⟪": 326,493 "⟫": 327,494 "⟮": 328,495 "⟯": 329,496 "⟶": 330,497 "⟹": 331,498 "⤳": 332,499 "⥤": 333,500 "⦃": 334,501 "⦄": 335,502 "⧏": 336,503 "⧸": 337,504 "⨁": 338,505 "⨂": 339,506 "⨅": 340,507 "⨆": 341,508 "⨍": 342,509 "⨯": 343,510 "⨳": 344,511 "⨿": 345,512 "⩿": 346,513 "⬝": 347,514 "￢": 348,515 "𝐞": 349,516 "𝑳": 350,517 "𝑹": 351,518 "𝒄": 352,519 "𝒅": 353,520 "𝒜": 354,521 "𝒞": 355,522 "𝒟": 356,523 "𝒢": 357,524 "𝒥": 358,525 "𝒪": 359,526 "𝒫": 360,527 "𝒮": 361,528 "𝒯": 362,529 "𝒰": 363,530 "𝒳": 364,531 "𝒴": 365,532 "𝒵": 366,533 "𝓐": 367,534 "𝓑": 368,535 "𝓒": 369,536 "𝓓": 370,537 "𝓕": 371,538 "𝓘": 372,539 "𝓚": 373,540 "𝓜": 374,541 "𝓝": 375,542 "𝓞": 376,543 "𝓟": 377,544 "𝓢": 378,545 "𝓤": 379,546 "𝓥": 380,547 "𝓦": 381,548 "𝔖": 382,549 "𝔗": 383,550 "𝔠": 384,551 "𝔪": 385,552 "𝔭": 386,553 "𝔸": 387,554 "𝔹": 388,555 "𝔻": 389,556 "𝔽": 390,557 "𝕂": 391,558 "𝕆": 392,559 "𝕊": 393,560 "𝕌": 394,561 "𝕎": 395,562 "𝕜": 396,563 "𝕝": 397,564 "𝖣": 398,565 "𝟙": 399,566 "𝟭": 400,567 "##l": 401,568 "##i": 402,569 "##q": 403,570 "##u": 404,571 "##e": 405,572 "##F": 406,573 "##r": 407,574 "##J": 408,575 "##x": 409,576 "##t": 410,577 "##n": 411,578 "##d": 412,579 "##R": 413,580 "##s": 414,581 "##c": 415,582 "##S": 416,583 "##a": 417,584 "##A": 418,585 "##j": 419,586 "##w": 420,587 "##T": 421,588 "##o": 422,589 "##O": 423,590 "##p": 424,591 "##L": 425,592 "##C": 426,593 "##v": 427,594 "##Ψ": 428,595 "##h": 429,596 "##y": 430,597 "##m": 431,598 "##M": 432,599 "##g": 433,600 "##σ": 434,601 "##1": 435,602 "##f": 436,603 "##E": 437,604 "##Z": 438,605 "##₀": 439,606 "##✝": 440,607 "##N": 441,608 "##H": 442,609 "##G": 443,610 "##₁": 444,611 "##X": 445,612 "##P": 446,613 "##b": 447,614 "##U": 448,615 "##2": 449,616 "##B": 450,617 "##₂": 451,618 "##⁻": 452,619 "##⁰": 453,620 "##D": 454,621 "##¹": 455,622 "##ζ": 456,623 "##k": 457,624 "##8": 458,625 "##7": 459,626 "##₅": 460,627 "##0": 461,628 "##₄": 462,629 "##I": 463,630 "##Q": 464,631 "##δ": 465,632 "##ε": 466,633 "##6": 467,634 "##3": 468,635 "##z": 469,636 "##₃": 470,637 "##𝒜": 471,638 "##K": 472,639 "##↑": 473,640 "##5": 474,641 "##θ": 475,642 "##V": 476,643 "##9": 477,644 "##ν": 478,645 "##μ": 479,646 "##₆": 480,647 "##4": 481,648 "##⋆": 482,649 "##W": 483,650 "##ᵒ": 484,651 "##ᵈ": 485,652 "##Δ": 486,653 "##π": 487,654 "##ᵀ": 488,655 "##Y": 489,656 "##√": 490,657 "##ξ": 491,658 "##ᵃ": 492,659 "##ₙ": 493,660 "##ₐ": 494,661 "##ₚ": 495,662 "##ₛ": 496,663 "##β": 497,664 "##⁺": 498,665 "##ᵐ": 499,666 "##φ": 500,667 "##ι": 501,668 "##Φ": 502,669 "##⁴": 503,670 "##⁵": 504,671 "##≥": 505,672 "##ᶜ": 506,673 "##ᗮ": 507,674 "##ᵣ": 508,675 "##⋯": 509,676 "##ω": 510,677 "##ᵢ": 511,678 "##γ": 512,679 "##α": 513,680 "##ₘ": 514,681 "##ᵛ": 515,682 "##ℒ": 516,683 "##ₑ": 517,684 "##ₒ": 518,685 "##³": 519,686 "##𝓝": 520,687 "##ψ": 521,688 "##₇": 522,689 "##ᴬ": 523,690 "##ᴹ": 524,691 "##ᵖ": 525,692 "##Γ": 526,693 "##◃": 527,694 "##♯": 528,695 "##ᴴ": 529,696 "##⁸": 530,697 "##ℱ": 531,698 "##χ": 532,699 "##𝒰": 533,700 "##￢": 534,701 "##⁷": 535,702 "##ˢ": 536,703 "##ʸ": 537,704 "##²": 538,705 "##ₗ": 539,706 "##ˣ": 540,707 "##𝖣": 541,708 "##∞": 542,709 "##ϕ": 543,710 "##∅": 544,711 "##⁄": 545,712 "##✶": 546,713 "##⊤": 547,714 "##ᶠ": 548,715 "##ᵇ": 549,716 "##ⁱ": 550,717 "##₈": 551,718 "##ᘁ": 552,719 "##η": 553,720 "##∂": 554,721 "##𝒄": 555,722 "##τ": 556,723 "##∀": 557,724 "##ϖ": 558,725 "##Λ": 559,726 "##𝕜": 560,727 "##∗": 561,728 "##κ": 562,729 "##Ω": 563,730 "##ℵ": 564,731 "##⊗": 565,732 "##⁹": 566,733 "##₉": 567,734 "##ₜ": 568,735 "##ρ": 569,736 "##ₖ": 570,737 "##⨅": 571,738 "##Θ": 572,739 "##⁶": 573,740 "##ᴸ": 574,741 "##∫": 575,742 "##𝟙": 576,743 "##ℂ": 577,744 "##𝓕": 578,745 "##ℝ": 579,746 "##𝔖": 580,747 "##ℬ": 581,748 "##¬": 582,749 "##⊥": 583,750 "##ℓ": 584,751 "##≫": 585,752 "##ᵁ": 586,753 "##𝓘": 587,754 "##ᵥ": 588,755 "##⋙": 589,756 "##∃": 590,757 "##𝒢": 591,758 "##ℙ": 592,759 "##𝔭": 593,760 "##ℤ": 594,761 "##ₕ": 595,762 "##∏": 596,763 "##∼": 597,764 "##⨆": 598,765 "##ᵤ": 599,766 "##𝕊": 600,767 "##λ": 601,768 "##⅟": 602,769 "##⋃": 603,770 "##̂": 604,771 "##∑": 605,772 "##∩": 606,773 "##𝕎": 607,774 "##⋂": 608,775 "##ℋ": 609,776 "VA": 610,777 "VAR": 611,778 "##pe": 612,779 "##ype": 613,780 "Type": 614,781 "##st": 615,782 "##or": 616,783 "in": 617,784 "inst": 618,785 "inst✝": 619,786 "##in": 620,787 "##om": 621,788 "GO": 622,789 "##AL": 623,790 "GOAL": 624,791 "##te": 625,792 "##al": 626,793 "##on": 627,794 "##le": 628,795 "##ory": 629,796 "##ac": 630,797 "##ro": 631,798 "##pac": 632,799 "##et": 633,800 "##as": 634,801 "##pace": 635,802 "##Space": 636,803 "##ed": 637,804 "##er": 638,805 "##omm": 639,806 "##ra": 640,807 "##un": 641,808 "##teg": 642,809 "##dd": 643,810 "##ing": 644,811 "##orm": 645,812 "##ti": 646,813 "##ateg": 647,814 "##ategory": 648,815 "##up": 649,816 "##he": 650,817 "##ar": 651,818 "Category": 652,819 "##re": 653,820 "##ic": 654,821 "##ble": 655,822 "##ormed": 656,823 "##eas": 657,824 "##roup": 658,825 "##ol": 659,826 "inst✝¹": 660,827 "##easu": 661,828 "##The": 662,829 "##Theory": 663,830 "##Comm": 664,831 "Is": 665,832 "##ddComm": 666,833 "Normed": 667,834 "##ap": 668,835 "##id": 669,836 "##Group": 670,837 "##ge": 671,838 "Set": 672,839 "##it": 673,840 "##op": 674,841 "##od": 675,842 "Measu": 676,843 "CategoryTheory": 677,844 "fun": 678,845 "Fin": 679,846 "##el": 680,847 "##ddCommGroup": 681,848 "##og": 682,849 "##en": 683,850 "##im": 684,851 "##em": 685,852 "##olog": 686,853 "##an": 687,854 "##odu": 688,855 "##odule": 689,856 "##at": 690,857 "##ul": 691,858 "##rable": 692,859 "##iv": 693,860 "##ct": 694,861 "inst✝²": 695,862 "##ono": 696,863 "##tion": 697,864 "##opolog": 698,865 "##Ring": 699,866 "##is": 700,867 "##ical": 701,868 "##bra": 702,869 "##gebra": 703,870 "##omp": 704,871 "##onoid": 705,872 "Comm": 706,873 "##AddCommGroup": 707,874 "##ec": 708,875 "##opological": 709,876 "##lgebra": 710,877 "##der": 711,878 "map": 712,879 "Topological": 713,880 "##ir": 714,881 "Module": 715,882 "TopologicalSpace": 716,883 "##ub": 717,884 "Measurable": 718,885 "NormedAddCommGroup": 719,886 "inst✝³": 720,887 "##able": 721,888 "to": 722,889 "##if": 723,890 "##ont": 724,891 "Measure": 725,892 "##il": 726,893 "##rder": 727,894 "##ve": 728,895 "##os": 729,896 "##ine": 730,897 "NormedSpace": 731,898 "##set": 732,899 "hf": 733,900 "##iring": 734,901 "##emiring": 735,902 "##Monoid": 736,903 "##ter": 737,904 "##iel": 738,905 "##ield": 739,906 "##Eq": 740,907 "##oc": 741,908 "##ite": 742,909 "inst✝⁴": 743,910 "CommRing": 744,911 "##ist": 745,912 "##ial": 746,913 "Algebra": 747,914 "MeasurableSpace": 748,915 "In": 749,916 "##eal": 750,917 "##bj": 751,918 "##inear": 752,919 "##us": 753,920 "Has": 754,921 "##Map": 755,922 "##rod": 756,923 "##omple": 757,924 "##ef": 758,925 "##uo": 759,926 "##um": 760,927 "##imit": 761,928 "##ith": 762,929 "Sub": 763,930 "##ly": 764,931 "##ecid": 765,932 "##Order": 766,933 "##Hom": 767,934 "##ig": 768,935 "##ecidable": 769,936 "Finset": 770,937 "##ric": 771,938 "Decidable": 772,939 "##ot": 773,940 "##uct": 774,941 "inst✝⁵": 775,942 "##In": 776,943 "##type": 777,944 "##his": 778,945 "##ie": 779,946 "##ilter": 780,947 "##tive": 781,948 "##ero": 782,949 "obj": 783,950 "##iz": 784,951 "AddCommGroup": 785,952 "##Cl": 786,953 "##ard": 787,954 "##On": 788,955 "##Fun": 789,956 "##With": 790,957 "##ort": 791,958 "##se": 792,959 "Add": 793,960 "##pp": 794,961 "##ction": 795,962 "##ontin": 796,963 "##Mul": 797,964 "##uous": 798,965 "##ontinuous": 799,966 "##ctor": 800,967 "DecidableEq": 801,968 "Fun": 802,969 "##ange": 803,970 "Linear": 804,971 "##Semiring": 805,972 "MeasureTheory": 806,973 "inst✝⁶": 807,974 "Pre": 808,975 "##ri": 809,976 "##At": 810,977 "hs": 811,978 "Fintype": 812,979 "##ation": 813,980 "##imits": 814,981 "##ddCommMonoid": 815,982 "re": 816,983 "Pro": 817,984 "##oun": 818,985 "##Measu": 819,986 "Non": 820,987 "##Field": 821,988 "##ow": 822,989 "hom": 823,990 "##tr": 824,991 "##rim": 825,992 "u₁": 826,993 "un": 827,994 "Filter": 828,995 "##uiv": 829,996 "AddCommMonoid": 830,997 "Mul": 831,998 "hx": 832,999 "##pen": 833,1000 "##ted": 834,1001 "List": 835,1002 "##igh": 836,1003 "##ens": 837,1004 "##ty": 838,1005 "##oly": 839,1006 "##eg": 840,1007 "##≥0": 841,1008 "##Zero": 842,1009 "comp": 843,1010 "##cc": 844,1011 "card": 845,1012 "ℝ≥0": 846,1013 "##Un": 847,1014 "##Fin": 848,1015 "Continuous": 849,1016 "##mm": 850,1017 "this": 851,1018 "range": 852,1019 "Limits": 853,1020 "##ass": 854,1021 "##ight": 855,1022 "Comple": 856,1023 "##riv": 857,1024 "##eft": 858,1025 "##Set": 859,1026 "##ocal": 860,1027 "##ift": 861,1028 "mk": 862,1029 "inst✝⁷": 863,1030 "##rivial": 864,1031 "Semiring": 865,1032 "##ion": 866,1033 "##ner": 867,1034 "app": 868,1035 "of": 869,1036 "hp": 870,1037 "##oin": 871,1038 "##omial": 872,1039 "##ent": 873,1040 "Field": 874,1041 "Ring": 875,1042 "##etric": 876,1043 "##Add": 877,1044 "ha": 878,1045 "##act": 879,1046 "Prop": 880,1047 "##pty": 881,1048 "Finite": 882,1049 "##ymm": 883,1050 "##ur": 884,1051 "##ree": 885,1052 "##nd": 886,1053 "CommSemiring": 887,1054 "IsS": 888,1055 "Lie": 889,1056 "##ontrivial": 890,1057 "Nontrivial": 891,1058 "##nomial": 892,1059 "##olynomial": 893,1060 "Subm": 894,1061 "##ower": 895,1062 "##roduct": 896,1063 "##har": 897,1064 "##deal": 898,1065 "##Of": 899,1066 "##Class": 900,1067 "M₂": 901,1068 "⁻¹": 902,1069 "##Real": 903,1070 "x✝": 904,1071 "##ce": 905,1072 "##ure": 906,1073 "Nat": 907,1074 "##Comple": 908,1075 "##rime": 909,1076 "##Sub": 910,1077 "symm": 911,1078 "Monoid": 912,1079 "Sem": 913,1080 "op": 914,1081 "##ain": 915,1082 "##eriv": 916,1083 "LinearOrder": 917,1084 "##empty": 918,1085 "inv": 919,1086 "↑n": 920,1087 "inst✝⁸": 921,1088 "##Is": 922,1089 "hg": 923,1090 "##end": 924,1091 "Nonempty": 925,1092 "##sto": 926,1093 "##endsto": 927,1094 "Function": 928,1095 "##upp": 929,1096 "##oot": 930,1097 "Sort": 931,1098 "##Algebra": 932,1099 "##rict": 933,1100 "Tendsto": 934,1101 "##jec": 935,1102 "Order": 936,1103 "##Unit": 937,1104 "Un": 938,1105 "co": 939,1106 "##de": 940,1107 "##iff": 941,1108 "##oint": 942,1109 "##Equiv": 943,1110 "##Finite": 944,1111 "##one": 945,1112 "∂μ": 946,1113 "##Top": 947,1114 "##ization": 948,1115 "Group": 949,1116 "v₁": 950,1117 "##truct": 951,1118 "##Product": 952,1119 "##Normed": 953,1120 "##hea": 954,1121 "##heaf": 955,1122 "ℝ≥0∞": 956,1123 "##jective": 957,1124 "##osed": 958,1125 "##asis": 959,1126 "St": 960,1127 "##eq": 961,1128 "##NormedField": 962,1129 "##ax": 963,1130 "##dj": 964,1131 "##lyNormedField": 965,1132 "Complete": 966,1133 "NontriviallyNormedField": 967,1134 "##ver": 968,1135 "##th": 969,1136 "##arti": 970,1137 "##ucc": 971,1138 "##ke": 972,1139 "IsC": 973,1140 "u₂": 974,1141 "##Measure": 975,1142 "##Complex": 976,1143 "##val": 977,1144 "val": 978,1145 "##pan": 979,1146 "at": 980,1147 "##ss": 981,1148 "##cal": 982,1149 "inst✝⁹": 983,1150 "##Deriv": 984,1151 "M₁": 985,1152 "↑x": 986,1153 "##ran": 987,1154 "##ount": 988,1155 "##ph": 989,1156 "##itive": 990,1157 "##etricSpace": 991,1158 "##ian": 992,1159 "##ors": 993,1160 "cl": 994,1161 "##all": 995,1162 "IsL": 996,1163 "##ull": 997,1164 "##Measurable": 998,1165 "hn": 999,1166 "Semin": 1000,1167 "##ple": 1001,1168 "##Category": 1002,1169 "##Iso": 1003,1170 "##ual": 1004,1171 "##inal": 1005,1172 "Mat": 1006,1173 "##calar": 1007,1174 "##ad": 1008,1175 "##ma": 1009,1176 "##ate": 1010,1177 "Submodule": 1011,1178 "##iform": 1012,1179 "##opology": 1013,1180 "##am": 1014,1181 "algebra": 1015,1182 "Ideal": 1016,1183 "##Li": 1017,1184 "algebraMap": 1018,1185 "##rix": 1019,1186 "##order": 1020,1187 "##Like": 1021,1188 "##ff": 1022,1189 "prod": 1023,1190 "##ern": 1024,1191 "##ser": 1025,1192 "Preorder": 1026,1193 "##ompac": 1027,1194 "##ompact": 1028,1195 "##Topology": 1029,1196 "con": 1030,1197 "##xp": 1031,1198 "Seminormed": 1032,1199 "⇑f": 1033,1200 "f₁": 1034,