| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1487 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1124 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (127 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (31 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (104 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |
Global Index
A
AC_equiv' [lemma, in Sierpinski.Sierpinski]AC_equiv [lemma, in Sierpinski.Sierpinski]
adjunction [definition, in Sierpinski.Basics]
All [definition, in Sierpinski.Basics]
Any [definition, in Sierpinski.Basics]
Axiom_Of_Choice'' [definition, in Sierpinski.Sierpinski]
Axiom_Of_Choice' [definition, in Sierpinski.Sierpinski]
Axiom_Of_Choice [definition, in Sierpinski.Sierpinski]
A':104 [binder, in Sierpinski.Basics]
A':109 [binder, in Sierpinski.Basics]
A':114 [binder, in Sierpinski.Basics]
A':122 [binder, in Sierpinski.Basics]
A':124 [binder, in Sierpinski.Basics]
a':168 [binder, in Sierpinski.Ordinals]
A':168 [binder, in Sierpinski.Cardinality]
A':172 [binder, in Sierpinski.Cardinality]
a':200 [binder, in Sierpinski.Basics]
A':230 [binder, in Sierpinski.Ordinals]
A':238 [binder, in Sierpinski.Ordinals]
a':445 [binder, in Sierpinski.Basics]
A':58 [binder, in Sierpinski.Ordinals]
a':60 [binder, in Sierpinski.Ordinals]
a':63 [binder, in Sierpinski.Ordinals]
a':66 [binder, in Sierpinski.Ordinals]
a':67 [binder, in Sierpinski.Ordinals]
a':68 [binder, in Sierpinski.Ordinals]
A':71 [binder, in Sierpinski.Ordinals]
a':73 [binder, in Sierpinski.Ordinals]
A':73 [binder, in Sierpinski.Basics]
a':75 [binder, in Sierpinski.Ordinals]
a1:104 [binder, in Sierpinski.Ordinals]
a1:13 [binder, in Sierpinski.Ordinals]
a1:23 [binder, in Sierpinski.Ordinals]
a1:4 [binder, in Sierpinski.Ordinals]
a1:40 [binder, in Sierpinski.Ordinals]
A1:56 [binder, in Sierpinski.Sierpinski]
A1:58 [binder, in Sierpinski.Sierpinski]
A1:60 [binder, in Sierpinski.Sierpinski]
A1:62 [binder, in Sierpinski.Sierpinski]
A1:76 [binder, in Sierpinski.Basics]
a1:9 [binder, in Sierpinski.Ordinals]
a2:10 [binder, in Sierpinski.Ordinals]
a2:105 [binder, in Sierpinski.Ordinals]
a2:14 [binder, in Sierpinski.Ordinals]
a2:24 [binder, in Sierpinski.Ordinals]
a2:41 [binder, in Sierpinski.Ordinals]
a2:5 [binder, in Sierpinski.Ordinals]
A2:57 [binder, in Sierpinski.Sierpinski]
A2:59 [binder, in Sierpinski.Sierpinski]
A2:64 [binder, in Sierpinski.Sierpinski]
A2:65 [binder, in Sierpinski.Sierpinski]
A2:77 [binder, in Sierpinski.Basics]
A:1 [binder, in Sierpinski.Ordinals]
A:1 [binder, in Sierpinski.Cardinality]
A:1 [binder, in Sierpinski.Sierpinski]
A:1 [binder, in Sierpinski.Hartogs]
A:10 [binder, in Sierpinski.Hartogs]
a:100 [binder, in Sierpinski.Basics]
a:101 [binder, in Sierpinski.Cardinality]
A:101 [binder, in Sierpinski.Basics]
a:104 [binder, in Sierpinski.Cardinality]
a:105 [binder, in Sierpinski.Basics]
A:106 [binder, in Sierpinski.Ordinals]
A:106 [binder, in Sierpinski.Basics]
a:107 [binder, in Sierpinski.Cardinality]
A:108 [binder, in Sierpinski.Cardinality]
A:11 [binder, in Sierpinski.Ordinals]
a:11 [binder, in Sierpinski.Cardinality]
A:11 [binder, in Sierpinski.Hartogs]
A:110 [binder, in Sierpinski.Cardinality]
A:111 [binder, in Sierpinski.Ordinals]
A:112 [binder, in Sierpinski.Basics]
A:114 [binder, in Sierpinski.Cardinality]
A:116 [binder, in Sierpinski.Cardinality]
A:117 [binder, in Sierpinski.Basics]
A:119 [binder, in Sierpinski.Ordinals]
A:119 [binder, in Sierpinski.Cardinality]
A:12 [binder, in Sierpinski.Hartogs]
A:123 [binder, in Sierpinski.Ordinals]
A:123 [binder, in Sierpinski.Basics]
A:125 [binder, in Sierpinski.Ordinals]
A:125 [binder, in Sierpinski.Basics]
a:128 [binder, in Sierpinski.Basics]
A:129 [binder, in Sierpinski.Basics]
A:13 [binder, in Sierpinski.Hartogs]
A:131 [binder, in Sierpinski.Ordinals]
a:132 [binder, in Sierpinski.Basics]
A:133 [binder, in Sierpinski.Basics]
A:135 [binder, in Sierpinski.Ordinals]
A:14 [binder, in Sierpinski.Basics]
A:141 [binder, in Sierpinski.Cardinality]
A:143 [binder, in Sierpinski.Cardinality]
A:143 [binder, in Sierpinski.Basics]
A:146 [binder, in Sierpinski.Cardinality]
a:149 [binder, in Sierpinski.Cardinality]
A:15 [binder, in Sierpinski.Ordinals]
A:15 [binder, in Sierpinski.Cardinality]
a:152 [binder, in Sierpinski.Cardinality]
A:156 [binder, in Sierpinski.Cardinality]
A:157 [binder, in Sierpinski.Cardinality]
A:16 [binder, in Sierpinski.Cardinality]
A:162 [binder, in Sierpinski.Cardinality]
A:162 [binder, in Sierpinski.Basics]
a:163 [binder, in Sierpinski.Cardinality]
A:164 [binder, in Sierpinski.Ordinals]
a:164 [binder, in Sierpinski.Cardinality]
a:165 [binder, in Sierpinski.Cardinality]
a:166 [binder, in Sierpinski.Cardinality]
a:167 [binder, in Sierpinski.Ordinals]
A:167 [binder, in Sierpinski.Cardinality]
a:169 [binder, in Sierpinski.Ordinals]
A:169 [binder, in Sierpinski.Basics]
A:170 [binder, in Sierpinski.Ordinals]
A:170 [binder, in Sierpinski.Cardinality]
A:172 [binder, in Sierpinski.Ordinals]
A:173 [binder, in Sierpinski.Basics]
A:174 [binder, in Sierpinski.Ordinals]
A:174 [binder, in Sierpinski.Cardinality]
A:176 [binder, in Sierpinski.Basics]
A:177 [binder, in Sierpinski.Cardinality]
a:178 [binder, in Sierpinski.Basics]
A:18 [binder, in Sierpinski.Ordinals]
A:18 [binder, in Sierpinski.Sierpinski]
a:180 [binder, in Sierpinski.Basics]
a:181 [binder, in Sierpinski.Basics]
A:182 [binder, in Sierpinski.Basics]
A:183 [binder, in Sierpinski.Cardinality]
A:188 [binder, in Sierpinski.Basics]
A:19 [binder, in Sierpinski.Cardinality]
A:19 [binder, in Sierpinski.Basics]
A:191 [binder, in Sierpinski.Basics]
A:194 [binder, in Sierpinski.Basics]
a:198 [binder, in Sierpinski.Basics]
a:199 [binder, in Sierpinski.Basics]
a:206 [binder, in Sierpinski.Basics]
A:21 [binder, in Sierpinski.Ordinals]
A:21 [binder, in Sierpinski.Sierpinski]
A:220 [binder, in Sierpinski.Basics]
A:223 [binder, in Sierpinski.Basics]
A:225 [binder, in Sierpinski.Basics]
A:228 [binder, in Sierpinski.Ordinals]
A:228 [binder, in Sierpinski.Basics]
A:229 [binder, in Sierpinski.Ordinals]
A:23 [binder, in Sierpinski.Cardinality]
A:233 [binder, in Sierpinski.Ordinals]
A:237 [binder, in Sierpinski.Ordinals]
A:240 [binder, in Sierpinski.Ordinals]
A:246 [binder, in Sierpinski.Ordinals]
A:25 [binder, in Sierpinski.Ordinals]
A:250 [binder, in Sierpinski.Ordinals]
A:27 [binder, in Sierpinski.Cardinality]
A:271 [binder, in Sierpinski.Basics]
A:275 [binder, in Sierpinski.Basics]
A:28 [binder, in Sierpinski.Ordinals]
A:285 [binder, in Sierpinski.Basics]
a:287 [binder, in Sierpinski.Basics]
a:288 [binder, in Sierpinski.Basics]
A:289 [binder, in Sierpinski.Basics]
A:29 [binder, in Sierpinski.Basics]
A:295 [binder, in Sierpinski.Basics]
A:3 [binder, in Sierpinski.Hartogs]
A:30 [binder, in Sierpinski.Sierpinski]
A:301 [binder, in Sierpinski.Basics]
A:305 [binder, in Sierpinski.Basics]
A:313 [binder, in Sierpinski.Basics]
a:314 [binder, in Sierpinski.Basics]
A:32 [binder, in Sierpinski.Cardinality]
A:320 [binder, in Sierpinski.Basics]
A:34 [binder, in Sierpinski.Ordinals]
A:348 [binder, in Sierpinski.Basics]
A:35 [binder, in Sierpinski.Cardinality]
A:35 [binder, in Sierpinski.Basics]
a:352 [binder, in Sierpinski.Basics]
A:354 [binder, in Sierpinski.Basics]
a:358 [binder, in Sierpinski.Basics]
A:359 [binder, in Sierpinski.Basics]
A:36 [binder, in Sierpinski.Ordinals]
A:363 [binder, in Sierpinski.Basics]
A:366 [binder, in Sierpinski.Basics]
A:38 [binder, in Sierpinski.Ordinals]
A:38 [binder, in Sierpinski.Cardinality]
A:382 [binder, in Sierpinski.Basics]
A:386 [binder, in Sierpinski.Basics]
A:39 [binder, in Sierpinski.Basics]
A:390 [binder, in Sierpinski.Basics]
A:396 [binder, in Sierpinski.Basics]
A:40 [binder, in Sierpinski.Cardinality]
A:402 [binder, in Sierpinski.Basics]
A:407 [binder, in Sierpinski.Basics]
A:413 [binder, in Sierpinski.Basics]
A:418 [binder, in Sierpinski.Basics]
A:42 [binder, in Sierpinski.Ordinals]
A:42 [binder, in Sierpinski.Cardinality]
A:42 [binder, in Sierpinski.Basics]
A:424 [binder, in Sierpinski.Basics]
a:427 [binder, in Sierpinski.Basics]
a:429 [binder, in Sierpinski.Basics]
A:43 [binder, in Sierpinski.Cardinality]
A:431 [binder, in Sierpinski.Basics]
A:432 [binder, in Sierpinski.Basics]
a:434 [binder, in Sierpinski.Basics]
A:436 [binder, in Sierpinski.Basics]
A:439 [binder, in Sierpinski.Basics]
A:442 [binder, in Sierpinski.Basics]
a:444 [binder, in Sierpinski.Basics]
A:446 [binder, in Sierpinski.Basics]
A:45 [binder, in Sierpinski.Cardinality]
A:450 [binder, in Sierpinski.Basics]
a:452 [binder, in Sierpinski.Basics]
A:454 [binder, in Sierpinski.Basics]
A:46 [binder, in Sierpinski.Basics]
a:461 [binder, in Sierpinski.Basics]
A:463 [binder, in Sierpinski.Basics]
a:470 [binder, in Sierpinski.Basics]
a:472 [binder, in Sierpinski.Basics]
A:474 [binder, in Sierpinski.Basics]
A:48 [binder, in Sierpinski.Cardinality]
A:480 [binder, in Sierpinski.Basics]
a:483 [binder, in Sierpinski.Basics]
A:486 [binder, in Sierpinski.Basics]
A:49 [binder, in Sierpinski.Basics]
A:492 [binder, in Sierpinski.Basics]
a:497 [binder, in Sierpinski.Basics]
A:498 [binder, in Sierpinski.Basics]
A:499 [binder, in Sierpinski.Basics]
A:5 [binder, in Sierpinski.Sierpinski]
a:502 [binder, in Sierpinski.Basics]
A:503 [binder, in Sierpinski.Basics]
a:507 [binder, in Sierpinski.Basics]
a:508 [binder, in Sierpinski.Basics]
A:509 [binder, in Sierpinski.Basics]
A:513 [binder, in Sierpinski.Basics]
A:517 [binder, in Sierpinski.Basics]
A:523 [binder, in Sierpinski.Basics]
A:529 [binder, in Sierpinski.Basics]
A:53 [binder, in Sierpinski.Cardinality]
A:53 [binder, in Sierpinski.Basics]
A:54 [binder, in Sierpinski.Cardinality]
A:54 [binder, in Sierpinski.Sierpinski]
A:543 [binder, in Sierpinski.Basics]
A:56 [binder, in Sierpinski.Ordinals]
A:564 [binder, in Sierpinski.Basics]
A:574 [binder, in Sierpinski.Basics]
a:583 [binder, in Sierpinski.Basics]
a:585 [binder, in Sierpinski.Basics]
a:587 [binder, in Sierpinski.Basics]
a:589 [binder, in Sierpinski.Basics]
a:59 [binder, in Sierpinski.Ordinals]
A:59 [binder, in Sierpinski.Cardinality]
a:591 [binder, in Sierpinski.Basics]
a:593 [binder, in Sierpinski.Basics]
A:6 [binder, in Sierpinski.Ordinals]
A:6 [binder, in Sierpinski.Cardinality]
a:61 [binder, in Sierpinski.Ordinals]
a:61 [binder, in Sierpinski.Sierpinski]
a:62 [binder, in Sierpinski.Ordinals]
A:62 [binder, in Sierpinski.Cardinality]
A:620 [binder, in Sierpinski.Basics]
A:622 [binder, in Sierpinski.Basics]
a:625 [binder, in Sierpinski.Basics]
A:629 [binder, in Sierpinski.Basics]
a:63 [binder, in Sierpinski.Sierpinski]
a:64 [binder, in Sierpinski.Ordinals]
A:64 [binder, in Sierpinski.Basics]
a:65 [binder, in Sierpinski.Ordinals]
A:65 [binder, in Sierpinski.Cardinality]
A:68 [binder, in Sierpinski.Basics]
A:69 [binder, in Sierpinski.Ordinals]
A:7 [binder, in Sierpinski.Basics]
a:72 [binder, in Sierpinski.Ordinals]
A:72 [binder, in Sierpinski.Basics]
a:74 [binder, in Sierpinski.Ordinals]
A:74 [binder, in Sierpinski.Cardinality]
A:75 [binder, in Sierpinski.Basics]
A:76 [binder, in Sierpinski.Ordinals]
A:76 [binder, in Sierpinski.Cardinality]
A:78 [binder, in Sierpinski.Cardinality]
a:78 [binder, in Sierpinski.Basics]
A:79 [binder, in Sierpinski.Cardinality]
A:82 [binder, in Sierpinski.Ordinals]
A:82 [binder, in Sierpinski.Cardinality]
A:83 [binder, in Sierpinski.Basics]
A:85 [binder, in Sierpinski.Cardinality]
A:87 [binder, in Sierpinski.Basics]
A:89 [binder, in Sierpinski.Ordinals]
A:90 [binder, in Sierpinski.Cardinality]
a:91 [binder, in Sierpinski.Cardinality]
a:92 [binder, in Sierpinski.Cardinality]
A:93 [binder, in Sierpinski.Cardinality]
A:93 [binder, in Sierpinski.Basics]
A:94 [binder, in Sierpinski.Ordinals]
A:97 [binder, in Sierpinski.Basics]
a:98 [binder, in Sierpinski.Cardinality]
A:99 [binder, in Sierpinski.Ordinals]
B
base:349 [binder, in Sierpinski.Basics]base:355 [binder, in Sierpinski.Basics]
base:360 [binder, in Sierpinski.Basics]
base:365 [binder, in Sierpinski.Basics]
base:369 [binder, in Sierpinski.Basics]
Basics [library]
big_union [axiom, in Sierpinski.Basics]
biject [definition, in Sierpinski.Basics]
Bijection [record, in Sierpinski.Cardinality]
bijection_subrelation_flipped_injection [instance, in Sierpinski.Cardinality]
bijection_subrelation_injection [instance, in Sierpinski.Cardinality]
bijection_to_injection [lemma, in Sierpinski.Cardinality]
bijection_is_injective [lemma, in Sierpinski.Cardinality]
bijection_relation_transitivity [lemma, in Sierpinski.Cardinality]
bijection_relation_symmetry [lemma, in Sierpinski.Cardinality]
bijection_relation_reflexivity [lemma, in Sierpinski.Cardinality]
bijection_relation_on_Set [definition, in Sierpinski.Cardinality]
bijection_relation [definition, in Sierpinski.Cardinality]
bijection_left_right [projection, in Sierpinski.Cardinality]
bijection_right_left [projection, in Sierpinski.Cardinality]
bijection_to_left [projection, in Sierpinski.Cardinality]
bijection_to_right [projection, in Sierpinski.Cardinality]
build_strict_well_order [constructor, in Sierpinski.Ordinals]
build_surjection [constructor, in Sierpinski.Cardinality]
build_injection [constructor, in Sierpinski.Cardinality]
build_bijection [constructor, in Sierpinski.Cardinality]
build_is_unique_solution [constructor, in Sierpinski.Basics]
build_element [constructor, in Sierpinski.Basics]
build_class [constructor, in Sierpinski.Basics]
b':449 [binder, in Sierpinski.Basics]
b1:244 [binder, in Sierpinski.Ordinals]
b2:245 [binder, in Sierpinski.Ordinals]
b:100 [binder, in Sierpinski.Cardinality]
B:101 [binder, in Sierpinski.Ordinals]
B:102 [binder, in Sierpinski.Basics]
b:103 [binder, in Sierpinski.Cardinality]
b:106 [binder, in Sierpinski.Cardinality]
B:107 [binder, in Sierpinski.Basics]
B:108 [binder, in Sierpinski.Ordinals]
B:109 [binder, in Sierpinski.Cardinality]
B:111 [binder, in Sierpinski.Cardinality]
B:112 [binder, in Sierpinski.Ordinals]
B:113 [binder, in Sierpinski.Basics]
B:115 [binder, in Sierpinski.Cardinality]
B:117 [binder, in Sierpinski.Cardinality]
B:118 [binder, in Sierpinski.Basics]
B:120 [binder, in Sierpinski.Cardinality]
B:121 [binder, in Sierpinski.Ordinals]
B:126 [binder, in Sierpinski.Basics]
B:127 [binder, in Sierpinski.Ordinals]
b:13 [binder, in Sierpinski.Cardinality]
B:130 [binder, in Sierpinski.Basics]
B:133 [binder, in Sierpinski.Ordinals]
B:142 [binder, in Sierpinski.Cardinality]
B:147 [binder, in Sierpinski.Cardinality]
b:150 [binder, in Sierpinski.Cardinality]
b:153 [binder, in Sierpinski.Cardinality]
B:158 [binder, in Sierpinski.Cardinality]
B:17 [binder, in Sierpinski.Cardinality]
B:184 [binder, in Sierpinski.Cardinality]
B:20 [binder, in Sierpinski.Cardinality]
b:207 [binder, in Sierpinski.Basics]
B:221 [binder, in Sierpinski.Basics]
B:224 [binder, in Sierpinski.Basics]
B:226 [binder, in Sierpinski.Basics]
B:229 [binder, in Sierpinski.Basics]
B:24 [binder, in Sierpinski.Cardinality]
B:241 [binder, in Sierpinski.Ordinals]
B:247 [binder, in Sierpinski.Ordinals]
B:251 [binder, in Sierpinski.Ordinals]
B:28 [binder, in Sierpinski.Cardinality]
B:280 [binder, in Sierpinski.Basics]
B:282 [binder, in Sierpinski.Basics]
B:302 [binder, in Sierpinski.Basics]
B:306 [binder, in Sierpinski.Basics]
B:33 [binder, in Sierpinski.Cardinality]
B:36 [binder, in Sierpinski.Cardinality]
B:383 [binder, in Sierpinski.Basics]
B:387 [binder, in Sierpinski.Basics]
B:39 [binder, in Sierpinski.Cardinality]
B:391 [binder, in Sierpinski.Basics]
B:397 [binder, in Sierpinski.Basics]
B:403 [binder, in Sierpinski.Basics]
B:408 [binder, in Sierpinski.Basics]
B:41 [binder, in Sierpinski.Cardinality]
B:414 [binder, in Sierpinski.Basics]
B:419 [binder, in Sierpinski.Basics]
B:425 [binder, in Sierpinski.Basics]
b:428 [binder, in Sierpinski.Basics]
B:43 [binder, in Sierpinski.Basics]
b:430 [binder, in Sierpinski.Basics]
B:433 [binder, in Sierpinski.Basics]
b:435 [binder, in Sierpinski.Basics]
B:437 [binder, in Sierpinski.Basics]
B:44 [binder, in Sierpinski.Cardinality]
B:440 [binder, in Sierpinski.Basics]
B:443 [binder, in Sierpinski.Basics]
B:447 [binder, in Sierpinski.Basics]
b:448 [binder, in Sierpinski.Basics]
B:451 [binder, in Sierpinski.Basics]
b:453 [binder, in Sierpinski.Basics]
B:455 [binder, in Sierpinski.Basics]
B:46 [binder, in Sierpinski.Cardinality]
b:462 [binder, in Sierpinski.Basics]
B:464 [binder, in Sierpinski.Basics]
b:471 [binder, in Sierpinski.Basics]
b:473 [binder, in Sierpinski.Basics]
B:475 [binder, in Sierpinski.Basics]
B:481 [binder, in Sierpinski.Basics]
B:487 [binder, in Sierpinski.Basics]
b:489 [binder, in Sierpinski.Basics]
B:49 [binder, in Sierpinski.Cardinality]
B:493 [binder, in Sierpinski.Basics]
b:496 [binder, in Sierpinski.Basics]
B:50 [binder, in Sierpinski.Basics]
B:500 [binder, in Sierpinski.Basics]
B:504 [binder, in Sierpinski.Basics]
B:510 [binder, in Sierpinski.Basics]
B:514 [binder, in Sierpinski.Basics]
b:516 [binder, in Sierpinski.Basics]
B:518 [binder, in Sierpinski.Basics]
b:521 [binder, in Sierpinski.Basics]
b:522 [binder, in Sierpinski.Basics]
B:524 [binder, in Sierpinski.Basics]
B:530 [binder, in Sierpinski.Basics]
B:54 [binder, in Sierpinski.Basics]
B:55 [binder, in Sierpinski.Cardinality]
B:55 [binder, in Sierpinski.Sierpinski]
B:565 [binder, in Sierpinski.Basics]
B:575 [binder, in Sierpinski.Basics]
B:6 [binder, in Sierpinski.Sierpinski]
B:60 [binder, in Sierpinski.Cardinality]
B:623 [binder, in Sierpinski.Basics]
b:626 [binder, in Sierpinski.Basics]
B:63 [binder, in Sierpinski.Cardinality]
B:630 [binder, in Sierpinski.Basics]
b:639 [binder, in Sierpinski.Basics]
b:640 [binder, in Sierpinski.Basics]
b:643 [binder, in Sierpinski.Basics]
b:644 [binder, in Sierpinski.Basics]
b:645 [binder, in Sierpinski.Basics]
b:646 [binder, in Sierpinski.Basics]
B:65 [binder, in Sierpinski.Basics]
B:66 [binder, in Sierpinski.Cardinality]
B:69 [binder, in Sierpinski.Basics]
B:7 [binder, in Sierpinski.Cardinality]
B:75 [binder, in Sierpinski.Cardinality]
B:77 [binder, in Sierpinski.Cardinality]
B:78 [binder, in Sierpinski.Ordinals]
B:80 [binder, in Sierpinski.Cardinality]
B:83 [binder, in Sierpinski.Cardinality]
B:84 [binder, in Sierpinski.Ordinals]
B:91 [binder, in Sierpinski.Ordinals]
B:94 [binder, in Sierpinski.Cardinality]
B:96 [binder, in Sierpinski.Ordinals]
b:97 [binder, in Sierpinski.Cardinality]
B:98 [binder, in Sierpinski.Basics]
C
cancel_inverse_left [lemma, in Sierpinski.Cardinality]cancel_inverse_right [lemma, in Sierpinski.Cardinality]
cantors_theorem [lemma, in Sierpinski.Cardinality]
Cardinality [library]
cartesian_product_upper_bound [lemma, in Sierpinski.Basics]
cartesian_product_eta [lemma, in Sierpinski.Basics]
cartesian_product [definition, in Sierpinski.Basics]
Class [record, in Sierpinski.Basics]
class_as_set_equiv_set [lemma, in Sierpinski.Cardinality]
class_as_set [definition, in Sierpinski.Cardinality]
class_of_all_sets [definition, in Sierpinski.Basics]
compose_isos [definition, in Sierpinski.Ordinals]
compose_injections [definition, in Sierpinski.Cardinality]
compose_bijections [definition, in Sierpinski.Cardinality]
comprehension [definition, in Sierpinski.Basics]
comprehension_condition [lemma, in Sierpinski.Basics]
conditional_fun_replacement [definition, in Sierpinski.Basics]
c:102 [binder, in Sierpinski.Cardinality]
c:105 [binder, in Sierpinski.Cardinality]
C:113 [binder, in Sierpinski.Ordinals]
C:119 [binder, in Sierpinski.Basics]
C:129 [binder, in Sierpinski.Ordinals]
C:29 [binder, in Sierpinski.Cardinality]
C:303 [binder, in Sierpinski.Basics]
C:456 [binder, in Sierpinski.Basics]
c:460 [binder, in Sierpinski.Basics]
C:465 [binder, in Sierpinski.Basics]
c:469 [binder, in Sierpinski.Basics]
C:47 [binder, in Sierpinski.Cardinality]
C:476 [binder, in Sierpinski.Basics]
C:482 [binder, in Sierpinski.Basics]
C:488 [binder, in Sierpinski.Basics]
c:554 [binder, in Sierpinski.Basics]
c:557 [binder, in Sierpinski.Basics]
C:56 [binder, in Sierpinski.Cardinality]
c:569 [binder, in Sierpinski.Basics]
C:81 [binder, in Sierpinski.Cardinality]
C:95 [binder, in Sierpinski.Cardinality]
c:96 [binder, in Sierpinski.Cardinality]
c:99 [binder, in Sierpinski.Cardinality]
D
decode [definition, in Sierpinski.Ordinals]decode_encode [lemma, in Sierpinski.Ordinals]
description [definition, in Sierpinski.Basics]
Description [section, in Sierpinski.Basics]
description_is_solution [lemma, in Sierpinski.Basics]
description_is_unique [instance, in Sierpinski.Basics]
difference [definition, in Sierpinski.Basics]
Disjoint [definition, in Sierpinski.Cardinality]
disjoint_union_is_increasing_on_right [lemma, in Sierpinski.Cardinality]
disjoint_union_is_increasing_on_left [lemma, in Sierpinski.Cardinality]
disjoint_union_associative [lemma, in Sierpinski.Cardinality]
disjoint_union_ind [definition, in Sierpinski.Basics]
disjoint_union_iter_reduction_right [lemma, in Sierpinski.Basics]
disjoint_union_iter_reduction_left [lemma, in Sierpinski.Basics]
disjoint_union_iter_property [lemma, in Sierpinski.Basics]
disjoint_union_iter [definition, in Sierpinski.Basics]
Disjoint_Union_Iter_Property [definition, in Sierpinski.Basics]
disjoint_union [definition, in Sierpinski.Basics]
E
element [abbreviation, in Sierpinski.Basics]elements1:257 [binder, in Sierpinski.Basics]
elements1:261 [binder, in Sierpinski.Basics]
elements2:258 [binder, in Sierpinski.Basics]
elements2:262 [binder, in Sierpinski.Basics]
elements:241 [binder, in Sierpinski.Basics]
elements:244 [binder, in Sierpinski.Basics]
elements:249 [binder, in Sierpinski.Basics]
elements:254 [binder, in Sierpinski.Basics]
element_relation_on_O_is_well_founded [instance, in Sierpinski.Ordinals]
element_of_ordinal_is_ordinal [instance, in Sierpinski.Ordinals]
element_of_tail_is_element_of_adjunction [instance, in Sierpinski.Basics]
element_stays_element [instance, in Sierpinski.Basics]
element_equality [lemma, in Sierpinski.Basics]
element_property [projection, in Sierpinski.Basics]
element_value [projection, in Sierpinski.Basics]
Element_Of [record, in Sierpinski.Basics]
element_predicate [projection, in Sierpinski.Basics]
empty_set_is_ordinal [instance, in Sierpinski.Ordinals]
empty_set_ind [lemma, in Sierpinski.Basics]
empty_set [axiom, in Sierpinski.Basics]
encode [definition, in Sierpinski.Ordinals]
encode_fun_el [lemma, in Sierpinski.Basics]
encode_funspace_firstorder [definition, in Sierpinski.Basics]
encode_funspace2 [definition, in Sierpinski.Basics]
encode_fun [definition, in Sierpinski.Basics]
encode_props [definition, in Sierpinski.Basics]
encodings [definition, in Sierpinski.Ordinals]
exists_element_of_explicit_set_iff [lemma, in Sierpinski.Basics]
explicit_set_equals_explicit_set_iff [lemma, in Sierpinski.Basics]
explicit_set_is_subset_of_explicit_set_iff [lemma, in Sierpinski.Basics]
explicit_set [definition, in Sierpinski.Basics]
extensionality [axiom, in Sierpinski.Basics]
extract_from_right_is_injective [lemma, in Sierpinski.Basics]
extract_from_right [definition, in Sierpinski.Basics]
extract_from_left [definition, in Sierpinski.Basics]
F
forall_elements_of_explicit_set_iff [lemma, in Sierpinski.Basics]foundation [definition, in Sierpinski.Basics]
from_left_or_right [lemma, in Sierpinski.Basics]
Functional [record, in Sierpinski.Basics]
Functional [inductive, in Sierpinski.Basics]
functionality [projection, in Sierpinski.Basics]
functionality [constructor, in Sierpinski.Basics]
function_compose_inverse [lemma, in Sierpinski.Cardinality]
fun_replacement_in_power_set [instance, in Sierpinski.Basics]
fun_replacement [definition, in Sierpinski.Basics]
f1:117 [binder, in Sierpinski.Ordinals]
f1:30 [binder, in Sierpinski.Cardinality]
f2:118 [binder, in Sierpinski.Ordinals]
f2:31 [binder, in Sierpinski.Cardinality]
f:103 [binder, in Sierpinski.Ordinals]
f:103 [binder, in Sierpinski.Basics]
f:108 [binder, in Sierpinski.Basics]
f:110 [binder, in Sierpinski.Ordinals]
f:115 [binder, in Sierpinski.Basics]
f:120 [binder, in Sierpinski.Basics]
f:127 [binder, in Sierpinski.Basics]
F:13 [binder, in Sierpinski.Sierpinski]
f:131 [binder, in Sierpinski.Basics]
f:136 [binder, in Sierpinski.Basics]
f:146 [binder, in Sierpinski.Basics]
f:18 [binder, in Sierpinski.Cardinality]
f:190 [binder, in Sierpinski.Ordinals]
f:21 [binder, in Sierpinski.Cardinality]
F:215 [binder, in Sierpinski.Ordinals]
F:219 [binder, in Sierpinski.Ordinals]
f:242 [binder, in Sierpinski.Ordinals]
f:248 [binder, in Sierpinski.Ordinals]
f:25 [binder, in Sierpinski.Cardinality]
f:252 [binder, in Sierpinski.Ordinals]
f:272 [binder, in Sierpinski.Basics]
f:276 [binder, in Sierpinski.Basics]
f:286 [binder, in Sierpinski.Basics]
f:290 [binder, in Sierpinski.Basics]
f:296 [binder, in Sierpinski.Basics]
f:31 [binder, in Sierpinski.Sierpinski]
f:34 [binder, in Sierpinski.Cardinality]
f:37 [binder, in Sierpinski.Cardinality]
f:534 [binder, in Sierpinski.Basics]
f:539 [binder, in Sierpinski.Basics]
f:544 [binder, in Sierpinski.Basics]
f:566 [binder, in Sierpinski.Basics]
f:57 [binder, in Sierpinski.Cardinality]
f:576 [binder, in Sierpinski.Basics]
f:599 [binder, in Sierpinski.Basics]
f:605 [binder, in Sierpinski.Basics]
f:609 [binder, in Sierpinski.Basics]
f:61 [binder, in Sierpinski.Cardinality]
f:613 [binder, in Sierpinski.Basics]
f:617 [binder, in Sierpinski.Basics]
f:624 [binder, in Sierpinski.Basics]
f:631 [binder, in Sierpinski.Basics]
f:64 [binder, in Sierpinski.Cardinality]
f:67 [binder, in Sierpinski.Cardinality]
f:8 [binder, in Sierpinski.Sierpinski]
f:84 [binder, in Sierpinski.Cardinality]
f:86 [binder, in Sierpinski.Ordinals]
f:88 [binder, in Sierpinski.Basics]
f:93 [binder, in Sierpinski.Ordinals]
f:94 [binder, in Sierpinski.Basics]
f:98 [binder, in Sierpinski.Ordinals]
f:99 [binder, in Sierpinski.Basics]
G
Generalized_Continuum_Hypothesis [definition, in Sierpinski.Sierpinski]Greater [definition, in Sierpinski.Ordinals]
g':633 [binder, in Sierpinski.Basics]
g:121 [binder, in Sierpinski.Basics]
g:567 [binder, in Sierpinski.Basics]
g:577 [binder, in Sierpinski.Basics]
g:58 [binder, in Sierpinski.Cardinality]
g:600 [binder, in Sierpinski.Basics]
g:606 [binder, in Sierpinski.Basics]
g:610 [binder, in Sierpinski.Basics]
g:614 [binder, in Sierpinski.Basics]
g:618 [binder, in Sierpinski.Basics]
g:632 [binder, in Sierpinski.Basics]
H
Hartogs [library]hartogs_number_has_upper_bound [lemma, in Sierpinski.Hartogs]
hartogs_number_is_not_smaller [lemma, in Sierpinski.Hartogs]
hartogs_number [definition, in Sierpinski.Hartogs]
hartogs_number_as_class_is_a_set [lemma, in Sierpinski.Hartogs]
hartogs_number_as_class_has_upper_bound [lemma, in Sierpinski.Hartogs]
hartogs_number_as_class [definition, in Sierpinski.Hartogs]
Has_Least_Elements [definition, in Sierpinski.Ordinals]
head_is_element_of_adjunction [instance, in Sierpinski.Basics]
H':528 [binder, in Sierpinski.Basics]
h':579 [binder, in Sierpinski.Basics]
H':6 [binder, in Sierpinski.Basics]
H0:146 [binder, in Sierpinski.Ordinals]
H:123 [binder, in Sierpinski.Cardinality]
H:124 [binder, in Sierpinski.Cardinality]
H:127 [binder, in Sierpinski.Cardinality]
H:128 [binder, in Sierpinski.Cardinality]
H:130 [binder, in Sierpinski.Cardinality]
H:131 [binder, in Sierpinski.Cardinality]
H:133 [binder, in Sierpinski.Cardinality]
H:134 [binder, in Sierpinski.Cardinality]
H:139 [binder, in Sierpinski.Basics]
H:144 [binder, in Sierpinski.Ordinals]
H:167 [binder, in Sierpinski.Basics]
H:17 [binder, in Sierpinski.Ordinals]
H:171 [binder, in Sierpinski.Cardinality]
H:172 [binder, in Sierpinski.Basics]
H:175 [binder, in Sierpinski.Cardinality]
H:178 [binder, in Sierpinski.Cardinality]
H:193 [binder, in Sierpinski.Basics]
H:20 [binder, in Sierpinski.Ordinals]
H:27 [binder, in Sierpinski.Ordinals]
H:3 [binder, in Sierpinski.Ordinals]
H:3 [binder, in Sierpinski.Cardinality]
H:325 [binder, in Sierpinski.Basics]
H:48 [binder, in Sierpinski.Basics]
H:5 [binder, in Sierpinski.Basics]
H:506 [binder, in Sierpinski.Basics]
H:520 [binder, in Sierpinski.Basics]
H:527 [binder, in Sierpinski.Basics]
h:568 [binder, in Sierpinski.Basics]
h:578 [binder, in Sierpinski.Basics]
h:634 [binder, in Sierpinski.Basics]
H:79 [binder, in Sierpinski.Ordinals]
H:8 [binder, in Sierpinski.Ordinals]
H:82 [binder, in Sierpinski.Basics]
H:91 [binder, in Sierpinski.Basics]
I
id_injection [definition, in Sierpinski.Cardinality]id_bijection [definition, in Sierpinski.Cardinality]
image_of_injection_is_equipotent [lemma, in Sierpinski.Cardinality]
image_of [definition, in Sierpinski.Basics]
image_under_id [lemma, in Sierpinski.Basics]
image_of_image [lemma, in Sierpinski.Basics]
image_under [definition, in Sierpinski.Basics]
indexed_intersection [definition, in Sierpinski.Basics]
indexed_union [definition, in Sierpinski.Basics]
Infinite [definition, in Sierpinski.Sierpinski]
Injection [record, in Sierpinski.Cardinality]
injection_relation_transitivity [lemma, in Sierpinski.Cardinality]
injection_relation_reflexivity [lemma, in Sierpinski.Cardinality]
injection_relation_on_Set [definition, in Sierpinski.Cardinality]
injection_relation [definition, in Sierpinski.Cardinality]
injection_as_bijection_into_image [definition, in Sierpinski.Cardinality]
injection_property [projection, in Sierpinski.Cardinality]
injection_fun [projection, in Sierpinski.Cardinality]
injective [definition, in Sierpinski.Basics]
inj1 [definition, in Sierpinski.Basics]
inj1_extract_from_left [lemma, in Sierpinski.Basics]
inj1_and_inj2_are_disjoint [lemma, in Sierpinski.Basics]
inj1_is_injective [lemma, in Sierpinski.Basics]
inj2 [definition, in Sierpinski.Basics]
inj2_is_injective [lemma, in Sierpinski.Basics]
intersection [definition, in Sierpinski.Basics]
inverse [definition, in Sierpinski.Basics]
inverse_compose_function [lemma, in Sierpinski.Cardinality]
inverse_bijection [definition, in Sierpinski.Cardinality]
inverse_flip [lemma, in Sierpinski.Basics]
inverse_surjective [lemma, in Sierpinski.Basics]
inverse_injective [lemma, in Sierpinski.Basics]
in_class_as_set_iff [lemma, in Sierpinski.Cardinality]
in_Numeral_iff [lemma, in Sierpinski.Basics]
in_Numeral_iff' [axiom, in Sierpinski.Basics]
in_difference_iff [lemma, in Sierpinski.Basics]
in_intersection_iff [lemma, in Sierpinski.Basics]
in_indexed_intersection_iff [lemma, in Sierpinski.Basics]
in_indexed_union [instance, in Sierpinski.Basics]
in_indexed_union_iff [lemma, in Sierpinski.Basics]
in_explicit_set_iff [lemma, in Sierpinski.Basics]
in_adjunction_iff [lemma, in Sierpinski.Basics]
in_union_intro_right [instance, in Sierpinski.Basics]
in_union_intro_left [instance, in Sierpinski.Basics]
in_union_intro2 [instance, in Sierpinski.Basics]
in_union_intro1 [instance, in Sierpinski.Basics]
in_union_iff [lemma, in Sierpinski.Basics]
in_provisional_singleton [lemma, in Sierpinski.Basics]
in_provisional_unordered_pair_iff [lemma, in Sierpinski.Basics]
in_comprehension_iff_typed [lemma, in Sierpinski.Basics]
in_comprehension_iff [lemma, in Sierpinski.Basics]
in_conditional_fun_replacement_iff [lemma, in Sierpinski.Basics]
in_image_of [instance, in Sierpinski.Basics]
in_image_under [instance, in Sierpinski.Basics]
in_image_iff [lemma, in Sierpinski.Basics]
in_fun_replacement_iff [lemma, in Sierpinski.Basics]
in_replacement_iff [axiom, in Sierpinski.Basics]
in_set_if_in_subset [instance, in Sierpinski.Basics]
in_power_set_iff [axiom, in Sierpinski.Basics]
in_big_union_iff [axiom, in Sierpinski.Basics]
in_empty_set_iff [axiom, in Sierpinski.Basics]
in_class_of_all_sets [instance, in Sierpinski.Basics]
in_class [projection, in Sierpinski.Basics]
In_Class [record, in Sierpinski.Basics]
in_class [constructor, in Sierpinski.Basics]
In_Class [inductive, in Sierpinski.Basics]
In_Set [axiom, in Sierpinski.Basics]
isomorphic_ordinals_are_equal [lemma, in Sierpinski.Ordinals]
Isomorphism [definition, in Sierpinski.Ordinals]
isomorphism_relation_symmetry [lemma, in Sierpinski.Ordinals]
isomorphism_relation_transitivity [lemma, in Sierpinski.Ordinals]
isomorphism_relation_reflexivity [lemma, in Sierpinski.Ordinals]
isomorphism_relation [definition, in Sierpinski.Ordinals]
isomorphism_inverse [definition, in Sierpinski.Ordinals]
isomorphism_preserves_relation [lemma, in Sierpinski.Ordinals]
isomorphism_to_bijection [definition, in Sierpinski.Ordinals]
Is_Limit [definition, in Sierpinski.Ordinals]
Is_Strict_Well_Order' [definition, in Sierpinski.Ordinals]
Is_Ordinal [inductive, in Sierpinski.Ordinals]
Is_Transitive_Set [definition, in Sierpinski.Ordinals]
Is_Trichotomous [definition, in Sierpinski.Ordinals]
Is_A_Set [definition, in Sierpinski.Cardinality]
Is_From_Right [definition, in Sierpinski.Basics]
Is_From_Left0:512 [binder, in Sierpinski.Basics]
Is_From_Left [definition, in Sierpinski.Basics]
Is_Unique_Solution_Of [record, in Sierpinski.Basics]
Is_Terminating [definition, in Sierpinski.Basics]
is_accessible_intro [constructor, in Sierpinski.Basics]
Is_Accessible_By [inductive, in Sierpinski.Basics]
Is_Subclass_Of [definition, in Sierpinski.Basics]
I:12 [binder, in Sierpinski.Sierpinski]
i:14 [binder, in Sierpinski.Sierpinski]
i:15 [binder, in Sierpinski.Sierpinski]
i:16 [binder, in Sierpinski.Sierpinski]
i:17 [binder, in Sierpinski.Sierpinski]
i:19 [binder, in Sierpinski.Sierpinski]
i:20 [binder, in Sierpinski.Sierpinski]
I:214 [binder, in Sierpinski.Ordinals]
i:216 [binder, in Sierpinski.Ordinals]
i:217 [binder, in Sierpinski.Ordinals]
I:218 [binder, in Sierpinski.Ordinals]
i:22 [binder, in Sierpinski.Sierpinski]
i:220 [binder, in Sierpinski.Ordinals]
i:23 [binder, in Sierpinski.Sierpinski]
i:38 [binder, in Sierpinski.Sierpinski]
i:39 [binder, in Sierpinski.Sierpinski]
i:40 [binder, in Sierpinski.Sierpinski]
i:42 [binder, in Sierpinski.Sierpinski]
i:44 [binder, in Sierpinski.Sierpinski]
i:45 [binder, in Sierpinski.Sierpinski]
i:46 [binder, in Sierpinski.Sierpinski]
i:47 [binder, in Sierpinski.Sierpinski]
i:48 [binder, in Sierpinski.Sierpinski]
i:49 [binder, in Sierpinski.Sierpinski]
i:50 [binder, in Sierpinski.Sierpinski]
i:51 [binder, in Sierpinski.Sierpinski]
i:52 [binder, in Sierpinski.Sierpinski]
i:53 [binder, in Sierpinski.Sierpinski]
L
least_element [definition, in Sierpinski.Ordinals]left_projection_beta [lemma, in Sierpinski.Basics]
left_projection [definition, in Sierpinski.Basics]
lemma1 [lemma, in Sierpinski.Sierpinski]
lemma2 [lemma, in Sierpinski.Sierpinski]
Less [definition, in Sierpinski.Ordinals]
Less_Or_Equal [definition, in Sierpinski.Cardinality]
linearity [lemma, in Sierpinski.Ordinals]
l_step:490 [binder, in Sierpinski.Basics]
l_step:484 [binder, in Sierpinski.Basics]
l_step:477 [binder, in Sierpinski.Basics]
l_step:466 [binder, in Sierpinski.Basics]
l_step:457 [binder, in Sierpinski.Basics]
l:15 [binder, in Sierpinski.Basics]
l:20 [binder, in Sierpinski.Basics]
N
nat_to_numeral_is_injective [lemma, in Sierpinski.Basics]nat_to_numeral_is_monotone [lemma, in Sierpinski.Basics]
nat_to_numeral_is_nat_to_numeral' [lemma, in Sierpinski.Basics]
nat_to_numeral [definition, in Sierpinski.Basics]
nat_to_numeral' [definition, in Sierpinski.Basics]
not_gt_implies_leq [lemma, in Sierpinski.Ordinals]
no_set_equals_its_power_set [lemma, in Sierpinski.Basics]
no_set_contains_itself [lemma, in Sierpinski.Basics]
Numeral [axiom, in Sierpinski.Basics]
Numeral_equipotent_Numeral_plus_one [lemma, in Sierpinski.Cardinality]
Numeral_iter_reduction_S [lemma, in Sierpinski.Basics]
Numeral_iter_reduction_O [lemma, in Sierpinski.Basics]
Numeral_iter_property [lemma, in Sierpinski.Basics]
Numeral_iter [definition, in Sierpinski.Basics]
Numeral_iter_Property [definition, in Sierpinski.Basics]
Numeral_ind [definition, in Sierpinski.Basics]
numeral_S [definition, in Sierpinski.Basics]
numeral_O [definition, in Sierpinski.Basics]
n':342 [binder, in Sierpinski.Basics]
n':344 [binder, in Sierpinski.Basics]
n0:353 [binder, in Sierpinski.Basics]
n:112 [binder, in Sierpinski.Cardinality]
n:113 [binder, in Sierpinski.Cardinality]
n:327 [binder, in Sierpinski.Basics]
n:332 [binder, in Sierpinski.Basics]
n:334 [binder, in Sierpinski.Basics]
n:335 [binder, in Sierpinski.Basics]
n:338 [binder, in Sierpinski.Basics]
n:340 [binder, in Sierpinski.Basics]
n:341 [binder, in Sierpinski.Basics]
n:343 [binder, in Sierpinski.Basics]
n:346 [binder, in Sierpinski.Basics]
n:347 [binder, in Sierpinski.Basics]
n:351 [binder, in Sierpinski.Basics]
n:357 [binder, in Sierpinski.Basics]
n:362 [binder, in Sierpinski.Basics]
n:367 [binder, in Sierpinski.Basics]
n:70 [binder, in Sierpinski.Sierpinski]
n:71 [binder, in Sierpinski.Sierpinski]
n:72 [binder, in Sierpinski.Sierpinski]
n:73 [binder, in Sierpinski.Sierpinski]
O
O [definition, in Sierpinski.Ordinals]one_ind [lemma, in Sierpinski.Basics]
Ordinals [library]
ordinal_induction [lemma, in Sierpinski.Ordinals]
ordinal_upper_bound [definition, in Sierpinski.Ordinals]
ordinal_is_element_iff_strict_sub [lemma, in Sierpinski.Ordinals]
ordinal_is_transitive' [instance, in Sierpinski.Ordinals]
ordinal_characterisation [lemma, in Sierpinski.Ordinals]
ordinal_is_transitive [lemma, in Sierpinski.Ordinals]
P
pair [definition, in Sierpinski.Basics]pair_is_injective_left [lemma, in Sierpinski.Basics]
pair_is_injective_right [lemma, in Sierpinski.Basics]
PE [axiom, in Sierpinski.Basics]
power_set_equiv_power_set_plus_power_set [lemma, in Sierpinski.Cardinality]
power_set_of_disjoint_union [lemma, in Sierpinski.Cardinality]
power_set_is_increasing [lemma, in Sierpinski.Cardinality]
power_set [axiom, in Sierpinski.Basics]
Preserves_Relation [definition, in Sierpinski.Ordinals]
proof_irrelevance [lemma, in Sierpinski.Basics]
provisional_singleton [definition, in Sierpinski.Basics]
provisional_unordered_pair [definition, in Sierpinski.Basics]
P_x:161 [binder, in Sierpinski.Basics]
P_x:159 [binder, in Sierpinski.Basics]
P_x:155 [binder, in Sierpinski.Basics]
P_x:153 [binder, in Sierpinski.Basics]
P_x:149 [binder, in Sierpinski.Basics]
P_x:140 [binder, in Sierpinski.Basics]
P:1 [binder, in Sierpinski.Basics]
P:134 [binder, in Sierpinski.Basics]
P:144 [binder, in Sierpinski.Basics]
P:16 [binder, in Sierpinski.Basics]
P:164 [binder, in Sierpinski.Basics]
P:166 [binder, in Sierpinski.Ordinals]
P:170 [binder, in Sierpinski.Basics]
P:174 [binder, in Sierpinski.Basics]
P:177 [binder, in Sierpinski.Basics]
P:196 [binder, in Sierpinski.Basics]
P:21 [binder, in Sierpinski.Basics]
P:223 [binder, in Sierpinski.Ordinals]
P:245 [binder, in Sierpinski.Basics]
P:250 [binder, in Sierpinski.Basics]
P:315 [binder, in Sierpinski.Basics]
P:321 [binder, in Sierpinski.Basics]
P:345 [binder, in Sierpinski.Basics]
P:370 [binder, in Sierpinski.Basics]
P:4 [binder, in Sierpinski.Basics]
P:44 [binder, in Sierpinski.Ordinals]
P:494 [binder, in Sierpinski.Basics]
P:545 [binder, in Sierpinski.Basics]
P:547 [binder, in Sierpinski.Basics]
P:60 [binder, in Sierpinski.Basics]
Q
Q:2 [binder, in Sierpinski.Basics]R
reflexive_closure_is_partial_order [instance, in Sierpinski.Ordinals]reflexive_closure_is_pre_order [instance, in Sierpinski.Ordinals]
reflexive_closure [definition, in Sierpinski.Ordinals]
replacement [axiom, in Sierpinski.Basics]
restrict_ordinal_isomorphism [definition, in Sierpinski.Ordinals]
restrict_well_order [definition, in Sierpinski.Ordinals]
right_projection_beta [lemma, in Sierpinski.Basics]
right_projection [definition, in Sierpinski.Basics]
R__B:134 [binder, in Sierpinski.Ordinals]
R__A:132 [binder, in Sierpinski.Ordinals]
R__C:130 [binder, in Sierpinski.Ordinals]
R__B:128 [binder, in Sierpinski.Ordinals]
R__A:126 [binder, in Sierpinski.Ordinals]
R__C:116 [binder, in Sierpinski.Ordinals]
R__B:115 [binder, in Sierpinski.Ordinals]
R__A:114 [binder, in Sierpinski.Ordinals]
r_step:491 [binder, in Sierpinski.Basics]
r_step:485 [binder, in Sierpinski.Basics]
r_step:478 [binder, in Sierpinski.Basics]
r_step:467 [binder, in Sierpinski.Basics]
r_step:458 [binder, in Sierpinski.Basics]
R':102 [binder, in Sierpinski.Ordinals]
R':109 [binder, in Sierpinski.Ordinals]
R':122 [binder, in Sierpinski.Ordinals]
R':85 [binder, in Sierpinski.Ordinals]
R':92 [binder, in Sierpinski.Ordinals]
R':97 [binder, in Sierpinski.Ordinals]
R:100 [binder, in Sierpinski.Ordinals]
R:107 [binder, in Sierpinski.Ordinals]
R:12 [binder, in Sierpinski.Ordinals]
R:120 [binder, in Sierpinski.Ordinals]
R:124 [binder, in Sierpinski.Ordinals]
R:16 [binder, in Sierpinski.Ordinals]
R:165 [binder, in Sierpinski.Ordinals]
R:171 [binder, in Sierpinski.Ordinals]
R:173 [binder, in Sierpinski.Ordinals]
R:183 [binder, in Sierpinski.Basics]
R:189 [binder, in Sierpinski.Basics]
R:19 [binder, in Sierpinski.Ordinals]
R:192 [binder, in Sierpinski.Basics]
R:195 [binder, in Sierpinski.Basics]
R:2 [binder, in Sierpinski.Ordinals]
R:2 [binder, in Sierpinski.Cardinality]
R:22 [binder, in Sierpinski.Ordinals]
R:231 [binder, in Sierpinski.Ordinals]
R:234 [binder, in Sierpinski.Ordinals]
R:239 [binder, in Sierpinski.Ordinals]
R:243 [binder, in Sierpinski.Ordinals]
R:249 [binder, in Sierpinski.Ordinals]
R:253 [binder, in Sierpinski.Ordinals]
R:26 [binder, in Sierpinski.Ordinals]
R:35 [binder, in Sierpinski.Ordinals]
R:37 [binder, in Sierpinski.Ordinals]
R:39 [binder, in Sierpinski.Ordinals]
R:43 [binder, in Sierpinski.Ordinals]
R:57 [binder, in Sierpinski.Ordinals]
R:7 [binder, in Sierpinski.Ordinals]
R:7 [binder, in Sierpinski.Sierpinski]
R:70 [binder, in Sierpinski.Ordinals]
R:77 [binder, in Sierpinski.Ordinals]
R:79 [binder, in Sierpinski.Basics]
R:8 [binder, in Sierpinski.Basics]
R:81 [binder, in Sierpinski.Basics]
R:83 [binder, in Sierpinski.Ordinals]
R:90 [binder, in Sierpinski.Ordinals]
R:95 [binder, in Sierpinski.Ordinals]
S
S [abbreviation, in Sierpinski.Basics]setlike [definition, in Sierpinski.Basics]
setlike_funspace_firstorder [lemma, in Sierpinski.Basics]
setlike_funspace_firstorder' [lemma, in Sierpinski.Basics]
setlike_setlike' [lemma, in Sierpinski.Basics]
setlike_power [lemma, in Sierpinski.Basics]
setlike_funspace2 [lemma, in Sierpinski.Basics]
setlike_sum [lemma, in Sierpinski.Basics]
setlike_prod [lemma, in Sierpinski.Basics]
setlike_Prop [lemma, in Sierpinski.Basics]
setlike_props [lemma, in Sierpinski.Basics]
setlike_nat [lemma, in Sierpinski.Basics]
setlike' [definition, in Sierpinski.Basics]
sets_are_well_founded [axiom, in Sierpinski.Basics]
set_equipotent_set_plus_one [lemma, in Sierpinski.Cardinality]
set_equipotent_subset_plus_difference [lemma, in Sierpinski.Cardinality]
set_equals_subset_union_difference [lemma, in Sierpinski.Cardinality]
set_in_power_set [instance, in Sierpinski.Basics]
set_to_class [definition, in Sierpinski.Basics]
Set_ [axiom, in Sierpinski.Basics]
Sierpinski [library]
sierpinskis_theorem [lemma, in Sierpinski.Sierpinski]
small_class_is_a_set [lemma, in Sierpinski.Cardinality]
solutions [definition, in Sierpinski.Basics]
step:350 [binder, in Sierpinski.Basics]
step:356 [binder, in Sierpinski.Basics]
step:361 [binder, in Sierpinski.Basics]
step:364 [binder, in Sierpinski.Basics]
step:368 [binder, in Sierpinski.Basics]
strict_well_order_is_strict_well_order' [lemma, in Sierpinski.Ordinals]
strict_well_order_on_ordinal [instance, in Sierpinski.Ordinals]
strict_well_order_on_O [instance, in Sierpinski.Ordinals]
strict_well_order_has_least_elements [lemma, in Sierpinski.Ordinals]
strict_well_order_has_least_elements' [lemma, in Sierpinski.Ordinals]
strict_well_order_is_strict_order [instance, in Sierpinski.Ordinals]
strict_well_order_as_function [definition, in Sierpinski.Ordinals]
strict_well_order_is_terminating [projection, in Sierpinski.Ordinals]
strict_well_order_is_trichotomous [projection, in Sierpinski.Ordinals]
strict_well_order_is_transitive [projection, in Sierpinski.Ordinals]
strict_well_order_relation [projection, in Sierpinski.Ordinals]
Strict_Well_Order_On [record, in Sierpinski.Ordinals]
strip_element [lemma, in Sierpinski.Basics]
subset_subrelation_injection [instance, in Sierpinski.Cardinality]
subset_extensionality [lemma, in Sierpinski.Basics]
subset_relation_transitivity [instance, in Sierpinski.Basics]
subset_relation_reflexivity [instance, in Sierpinski.Basics]
successor_ordinal [definition, in Sierpinski.Ordinals]
successor_is_ordinal [instance, in Sierpinski.Ordinals]
Surjection [record, in Sierpinski.Cardinality]
surjection_is_surjective [projection, in Sierpinski.Cardinality]
surjection_fun [projection, in Sierpinski.Cardinality]
surjective [definition, in Sierpinski.Basics]
symmetric_cartesian_product_is_increasing [lemma, in Sierpinski.Cardinality]
T
transitive_set_of_ordinals_is_ordinal [constructor, in Sierpinski.Ordinals]transported_relation_is_isomorphic [lemma, in Sierpinski.Ordinals]
transport_strict_well_order [definition, in Sierpinski.Ordinals]
transport_relation [definition, in Sierpinski.Ordinals]
two_is_power_set_of_one [lemma, in Sierpinski.Cardinality]
two_times_set_is_disjoin_union [lemma, in Sierpinski.Basics]
U
union [definition, in Sierpinski.Basics]union_is_ordinal [instance, in Sierpinski.Ordinals]
union_of_disjoints_equipotent_disjoint_union [lemma, in Sierpinski.Cardinality]
unique_solution_is_unique [projection, in Sierpinski.Basics]
unique_solution_is_solution [projection, in Sierpinski.Basics]
unordered_pair_equals_unordered_pair_iff [lemma, in Sierpinski.Basics]
untyped_pair_is_injective_right [lemma, in Sierpinski.Basics]
untyped_pair_is_injective_left [lemma, in Sierpinski.Basics]
untyped_pair [definition, in Sierpinski.Basics]
u:269 [binder, in Sierpinski.Basics]
u:309 [binder, in Sierpinski.Basics]
V
v:270 [binder, in Sierpinski.Basics]W
Well_Ordering_to_Choice [lemma, in Sierpinski.Sierpinski]Well_Ordering_to_Choice' [lemma, in Sierpinski.Sierpinski]
Well_Ordering_Theorem [definition, in Sierpinski.Sierpinski]
well_founded_induction [lemma, in Sierpinski.Basics]
wf:197 [binder, in Sierpinski.Basics]
X
x_in_A:157 [binder, in Sierpinski.Basics]x_in_A:151 [binder, in Sierpinski.Basics]
x_in_B:45 [binder, in Sierpinski.Basics]
x':152 [binder, in Sierpinski.Basics]
x':158 [binder, in Sierpinski.Basics]
x':375 [binder, in Sierpinski.Basics]
x':379 [binder, in Sierpinski.Basics]
x':393 [binder, in Sierpinski.Basics]
x':399 [binder, in Sierpinski.Basics]
x':422 [binder, in Sierpinski.Basics]
x':423 [binder, in Sierpinski.Basics]
x':526 [binder, in Sierpinski.Basics]
x':536 [binder, in Sierpinski.Basics]
x0:48 [binder, in Sierpinski.Ordinals]
x0:51 [binder, in Sierpinski.Ordinals]
x0:636 [binder, in Sierpinski.Basics]
x0:641 [binder, in Sierpinski.Basics]
x0:642 [binder, in Sierpinski.Basics]
x:10 [binder, in Sierpinski.Sierpinski]
x:10 [binder, in Sierpinski.Basics]
x:111 [binder, in Sierpinski.Basics]
x:116 [binder, in Sierpinski.Basics]
x:118 [binder, in Sierpinski.Cardinality]
x:121 [binder, in Sierpinski.Cardinality]
x:125 [binder, in Sierpinski.Cardinality]
x:129 [binder, in Sierpinski.Cardinality]
x:132 [binder, in Sierpinski.Cardinality]
x:135 [binder, in Sierpinski.Cardinality]
x:135 [binder, in Sierpinski.Basics]
x:136 [binder, in Sierpinski.Ordinals]
x:136 [binder, in Sierpinski.Cardinality]
x:137 [binder, in Sierpinski.Cardinality]
x:137 [binder, in Sierpinski.Basics]
x:138 [binder, in Sierpinski.Cardinality]
x:139 [binder, in Sierpinski.Cardinality]
x:140 [binder, in Sierpinski.Cardinality]
x:141 [binder, in Sierpinski.Ordinals]
x:141 [binder, in Sierpinski.Basics]
x:142 [binder, in Sierpinski.Basics]
x:145 [binder, in Sierpinski.Ordinals]
x:145 [binder, in Sierpinski.Basics]
x:148 [binder, in Sierpinski.Cardinality]
x:148 [binder, in Sierpinski.Basics]
x:149 [binder, in Sierpinski.Ordinals]
x:150 [binder, in Sierpinski.Basics]
x:151 [binder, in Sierpinski.Ordinals]
x:151 [binder, in Sierpinski.Cardinality]
x:153 [binder, in Sierpinski.Ordinals]
x:154 [binder, in Sierpinski.Cardinality]
x:154 [binder, in Sierpinski.Basics]
x:155 [binder, in Sierpinski.Ordinals]
x:155 [binder, in Sierpinski.Cardinality]
x:156 [binder, in Sierpinski.Basics]
x:157 [binder, in Sierpinski.Ordinals]
x:160 [binder, in Sierpinski.Basics]
x:163 [binder, in Sierpinski.Basics]
x:165 [binder, in Sierpinski.Basics]
x:168 [binder, in Sierpinski.Basics]
x:169 [binder, in Sierpinski.Cardinality]
x:171 [binder, in Sierpinski.Basics]
x:173 [binder, in Sierpinski.Cardinality]
x:175 [binder, in Sierpinski.Ordinals]
x:175 [binder, in Sierpinski.Basics]
x:176 [binder, in Sierpinski.Cardinality]
x:177 [binder, in Sierpinski.Ordinals]
x:179 [binder, in Sierpinski.Ordinals]
x:179 [binder, in Sierpinski.Cardinality]
x:179 [binder, in Sierpinski.Basics]
x:180 [binder, in Sierpinski.Cardinality]
x:181 [binder, in Sierpinski.Cardinality]
x:182 [binder, in Sierpinski.Ordinals]
x:182 [binder, in Sierpinski.Cardinality]
x:184 [binder, in Sierpinski.Basics]
x:186 [binder, in Sierpinski.Ordinals]
x:186 [binder, in Sierpinski.Cardinality]
x:188 [binder, in Sierpinski.Ordinals]
x:188 [binder, in Sierpinski.Cardinality]
x:189 [binder, in Sierpinski.Cardinality]
x:190 [binder, in Sierpinski.Basics]
x:191 [binder, in Sierpinski.Cardinality]
x:192 [binder, in Sierpinski.Ordinals]
x:193 [binder, in Sierpinski.Cardinality]
x:194 [binder, in Sierpinski.Ordinals]
x:194 [binder, in Sierpinski.Cardinality]
x:196 [binder, in Sierpinski.Ordinals]
x:197 [binder, in Sierpinski.Ordinals]
x:2 [binder, in Sierpinski.Sierpinski]
x:2 [binder, in Sierpinski.Hartogs]
x:201 [binder, in Sierpinski.Ordinals]
x:202 [binder, in Sierpinski.Basics]
x:203 [binder, in Sierpinski.Ordinals]
x:203 [binder, in Sierpinski.Basics]
x:204 [binder, in Sierpinski.Basics]
x:206 [binder, in Sierpinski.Ordinals]
x:208 [binder, in Sierpinski.Ordinals]
x:208 [binder, in Sierpinski.Basics]
x:211 [binder, in Sierpinski.Basics]
x:212 [binder, in Sierpinski.Basics]
x:214 [binder, in Sierpinski.Basics]
x:216 [binder, in Sierpinski.Basics]
x:219 [binder, in Sierpinski.Basics]
x:22 [binder, in Sierpinski.Cardinality]
x:222 [binder, in Sierpinski.Basics]
x:227 [binder, in Sierpinski.Basics]
x:230 [binder, in Sierpinski.Basics]
x:231 [binder, in Sierpinski.Basics]
x:233 [binder, in Sierpinski.Basics]
x:235 [binder, in Sierpinski.Ordinals]
x:236 [binder, in Sierpinski.Basics]
x:238 [binder, in Sierpinski.Basics]
x:24 [binder, in Sierpinski.Sierpinski]
x:246 [binder, in Sierpinski.Basics]
x:247 [binder, in Sierpinski.Basics]
x:248 [binder, in Sierpinski.Basics]
x:251 [binder, in Sierpinski.Basics]
x:252 [binder, in Sierpinski.Basics]
x:253 [binder, in Sierpinski.Basics]
x:255 [binder, in Sierpinski.Basics]
x:259 [binder, in Sierpinski.Basics]
x:26 [binder, in Sierpinski.Cardinality]
x:26 [binder, in Sierpinski.Sierpinski]
x:263 [binder, in Sierpinski.Basics]
x:265 [binder, in Sierpinski.Basics]
x:267 [binder, in Sierpinski.Basics]
x:273 [binder, in Sierpinski.Basics]
x:274 [binder, in Sierpinski.Basics]
x:278 [binder, in Sierpinski.Basics]
x:279 [binder, in Sierpinski.Basics]
x:28 [binder, in Sierpinski.Sierpinski]
x:28 [binder, in Sierpinski.Basics]
x:281 [binder, in Sierpinski.Basics]
x:283 [binder, in Sierpinski.Basics]
x:284 [binder, in Sierpinski.Basics]
x:29 [binder, in Sierpinski.Sierpinski]
x:291 [binder, in Sierpinski.Basics]
x:293 [binder, in Sierpinski.Basics]
x:294 [binder, in Sierpinski.Basics]
x:297 [binder, in Sierpinski.Basics]
x:299 [binder, in Sierpinski.Basics]
x:300 [binder, in Sierpinski.Basics]
x:304 [binder, in Sierpinski.Basics]
x:307 [binder, in Sierpinski.Basics]
x:310 [binder, in Sierpinski.Basics]
x:318 [binder, in Sierpinski.Basics]
x:32 [binder, in Sierpinski.Sierpinski]
x:32 [binder, in Sierpinski.Basics]
x:322 [binder, in Sierpinski.Basics]
x:323 [binder, in Sierpinski.Basics]
x:326 [binder, in Sierpinski.Basics]
x:33 [binder, in Sierpinski.Sierpinski]
x:33 [binder, in Sierpinski.Basics]
x:331 [binder, in Sierpinski.Basics]
x:339 [binder, in Sierpinski.Basics]
x:34 [binder, in Sierpinski.Sierpinski]
x:35 [binder, in Sierpinski.Sierpinski]
x:36 [binder, in Sierpinski.Sierpinski]
x:37 [binder, in Sierpinski.Sierpinski]
x:371 [binder, in Sierpinski.Basics]
x:372 [binder, in Sierpinski.Basics]
x:374 [binder, in Sierpinski.Basics]
x:378 [binder, in Sierpinski.Basics]
x:384 [binder, in Sierpinski.Basics]
x:388 [binder, in Sierpinski.Basics]
x:392 [binder, in Sierpinski.Basics]
x:398 [binder, in Sierpinski.Basics]
x:4 [binder, in Sierpinski.Cardinality]
x:4 [binder, in Sierpinski.Sierpinski]
x:4 [binder, in Sierpinski.Hartogs]
x:40 [binder, in Sierpinski.Basics]
x:405 [binder, in Sierpinski.Basics]
x:409 [binder, in Sierpinski.Basics]
x:41 [binder, in Sierpinski.Sierpinski]
x:417 [binder, in Sierpinski.Basics]
x:420 [binder, in Sierpinski.Basics]
x:43 [binder, in Sierpinski.Sierpinski]
x:438 [binder, in Sierpinski.Basics]
x:44 [binder, in Sierpinski.Basics]
x:441 [binder, in Sierpinski.Basics]
x:45 [binder, in Sierpinski.Ordinals]
x:459 [binder, in Sierpinski.Basics]
x:468 [binder, in Sierpinski.Basics]
x:47 [binder, in Sierpinski.Ordinals]
x:47 [binder, in Sierpinski.Basics]
x:479 [binder, in Sierpinski.Basics]
x:49 [binder, in Sierpinski.Ordinals]
x:495 [binder, in Sierpinski.Basics]
x:5 [binder, in Sierpinski.Hartogs]
x:501 [binder, in Sierpinski.Basics]
x:505 [binder, in Sierpinski.Basics]
x:51 [binder, in Sierpinski.Basics]
x:511 [binder, in Sierpinski.Basics]
x:515 [binder, in Sierpinski.Basics]
x:519 [binder, in Sierpinski.Basics]
x:52 [binder, in Sierpinski.Ordinals]
x:52 [binder, in Sierpinski.Basics]
x:525 [binder, in Sierpinski.Basics]
x:531 [binder, in Sierpinski.Basics]
X:532 [binder, in Sierpinski.Basics]
x:535 [binder, in Sierpinski.Basics]
X:537 [binder, in Sierpinski.Basics]
x:541 [binder, in Sierpinski.Basics]
X:542 [binder, in Sierpinski.Basics]
x:546 [binder, in Sierpinski.Basics]
x:548 [binder, in Sierpinski.Basics]
x:549 [binder, in Sierpinski.Basics]
x:55 [binder, in Sierpinski.Basics]
x:550 [binder, in Sierpinski.Basics]
x:551 [binder, in Sierpinski.Basics]
X:552 [binder, in Sierpinski.Basics]
x:555 [binder, in Sierpinski.Basics]
x:558 [binder, in Sierpinski.Basics]
X:560 [binder, in Sierpinski.Basics]
X:562 [binder, in Sierpinski.Basics]
x:570 [binder, in Sierpinski.Basics]
X:572 [binder, in Sierpinski.Basics]
x:58 [binder, in Sierpinski.Basics]
X:580 [binder, in Sierpinski.Basics]
X:582 [binder, in Sierpinski.Basics]
x:584 [binder, in Sierpinski.Basics]
x:586 [binder, in Sierpinski.Basics]
x:588 [binder, in Sierpinski.Basics]
x:590 [binder, in Sierpinski.Basics]
x:592 [binder, in Sierpinski.Basics]
x:594 [binder, in Sierpinski.Basics]
x:595 [binder, in Sierpinski.Basics]
x:596 [binder, in Sierpinski.Basics]
X:597 [binder, in Sierpinski.Basics]
x:6 [binder, in Sierpinski.Hartogs]
x:601 [binder, in Sierpinski.Basics]
X:603 [binder, in Sierpinski.Basics]
X:607 [binder, in Sierpinski.Basics]
x:61 [binder, in Sierpinski.Basics]
X:611 [binder, in Sierpinski.Basics]
X:615 [binder, in Sierpinski.Basics]
X:619 [binder, in Sierpinski.Basics]
X:621 [binder, in Sierpinski.Basics]
X:627 [binder, in Sierpinski.Basics]
x:63 [binder, in Sierpinski.Basics]
x:635 [binder, in Sierpinski.Basics]
X:637 [binder, in Sierpinski.Basics]
X:647 [binder, in Sierpinski.Basics]
x:66 [binder, in Sierpinski.Sierpinski]
x:68 [binder, in Sierpinski.Cardinality]
x:69 [binder, in Sierpinski.Cardinality]
x:71 [binder, in Sierpinski.Cardinality]
x:71 [binder, in Sierpinski.Basics]
x:73 [binder, in Sierpinski.Cardinality]
x:74 [binder, in Sierpinski.Basics]
x:8 [binder, in Sierpinski.Hartogs]
x:80 [binder, in Sierpinski.Ordinals]
x:85 [binder, in Sierpinski.Basics]
x:86 [binder, in Sierpinski.Cardinality]
x:87 [binder, in Sierpinski.Ordinals]
x:87 [binder, in Sierpinski.Cardinality]
x:88 [binder, in Sierpinski.Cardinality]
x:89 [binder, in Sierpinski.Cardinality]
x:89 [binder, in Sierpinski.Basics]
x:9 [binder, in Sierpinski.Sierpinski]
x:92 [binder, in Sierpinski.Basics]
x:96 [binder, in Sierpinski.Basics]
Y
y':12 [binder, in Sierpinski.Basics]y':377 [binder, in Sierpinski.Basics]
y':381 [binder, in Sierpinski.Basics]
y':395 [binder, in Sierpinski.Basics]
y':401 [binder, in Sierpinski.Basics]
y':411 [binder, in Sierpinski.Basics]
y':412 [binder, in Sierpinski.Basics]
y:11 [binder, in Sierpinski.Sierpinski]
y:11 [binder, in Sierpinski.Basics]
y:110 [binder, in Sierpinski.Basics]
y:122 [binder, in Sierpinski.Cardinality]
y:126 [binder, in Sierpinski.Cardinality]
y:137 [binder, in Sierpinski.Ordinals]
y:138 [binder, in Sierpinski.Basics]
y:144 [binder, in Sierpinski.Cardinality]
y:145 [binder, in Sierpinski.Cardinality]
y:147 [binder, in Sierpinski.Basics]
y:150 [binder, in Sierpinski.Ordinals]
y:152 [binder, in Sierpinski.Ordinals]
y:154 [binder, in Sierpinski.Ordinals]
y:156 [binder, in Sierpinski.Ordinals]
y:158 [binder, in Sierpinski.Ordinals]
y:166 [binder, in Sierpinski.Basics]
y:176 [binder, in Sierpinski.Ordinals]
y:178 [binder, in Sierpinski.Ordinals]
y:180 [binder, in Sierpinski.Ordinals]
y:183 [binder, in Sierpinski.Ordinals]
y:185 [binder, in Sierpinski.Cardinality]
y:187 [binder, in Sierpinski.Ordinals]
y:187 [binder, in Sierpinski.Cardinality]
y:187 [binder, in Sierpinski.Basics]
y:189 [binder, in Sierpinski.Ordinals]
y:190 [binder, in Sierpinski.Cardinality]
y:192 [binder, in Sierpinski.Cardinality]
y:193 [binder, in Sierpinski.Ordinals]
y:195 [binder, in Sierpinski.Ordinals]
y:198 [binder, in Sierpinski.Ordinals]
y:199 [binder, in Sierpinski.Ordinals]
y:200 [binder, in Sierpinski.Ordinals]
y:202 [binder, in Sierpinski.Ordinals]
y:205 [binder, in Sierpinski.Basics]
y:207 [binder, in Sierpinski.Ordinals]
y:209 [binder, in Sierpinski.Ordinals]
y:209 [binder, in Sierpinski.Basics]
y:213 [binder, in Sierpinski.Basics]
y:215 [binder, in Sierpinski.Basics]
y:217 [binder, in Sierpinski.Basics]
y:232 [binder, in Sierpinski.Basics]
y:234 [binder, in Sierpinski.Basics]
y:236 [binder, in Sierpinski.Ordinals]
y:237 [binder, in Sierpinski.Basics]
y:239 [binder, in Sierpinski.Basics]
y:25 [binder, in Sierpinski.Sierpinski]
y:256 [binder, in Sierpinski.Basics]
y:260 [binder, in Sierpinski.Basics]
y:264 [binder, in Sierpinski.Basics]
y:266 [binder, in Sierpinski.Basics]
y:268 [binder, in Sierpinski.Basics]
y:27 [binder, in Sierpinski.Sierpinski]
y:3 [binder, in Sierpinski.Sierpinski]
y:308 [binder, in Sierpinski.Basics]
y:311 [binder, in Sierpinski.Basics]
y:324 [binder, in Sierpinski.Basics]
y:34 [binder, in Sierpinski.Basics]
y:373 [binder, in Sierpinski.Basics]
y:376 [binder, in Sierpinski.Basics]
y:380 [binder, in Sierpinski.Basics]
y:385 [binder, in Sierpinski.Basics]
y:389 [binder, in Sierpinski.Basics]
y:394 [binder, in Sierpinski.Basics]
y:400 [binder, in Sierpinski.Basics]
y:406 [binder, in Sierpinski.Basics]
y:41 [binder, in Sierpinski.Basics]
y:410 [binder, in Sierpinski.Basics]
y:416 [binder, in Sierpinski.Basics]
y:421 [binder, in Sierpinski.Basics]
y:46 [binder, in Sierpinski.Ordinals]
y:5 [binder, in Sierpinski.Cardinality]
y:50 [binder, in Sierpinski.Ordinals]
y:53 [binder, in Sierpinski.Ordinals]
Y:533 [binder, in Sierpinski.Basics]
Y:538 [binder, in Sierpinski.Basics]
y:54 [binder, in Sierpinski.Ordinals]
y:540 [binder, in Sierpinski.Basics]
y:55 [binder, in Sierpinski.Ordinals]
Y:553 [binder, in Sierpinski.Basics]
y:556 [binder, in Sierpinski.Basics]
y:559 [binder, in Sierpinski.Basics]
Y:561 [binder, in Sierpinski.Basics]
Y:563 [binder, in Sierpinski.Basics]
y:571 [binder, in Sierpinski.Basics]
Y:573 [binder, in Sierpinski.Basics]
Y:581 [binder, in Sierpinski.Basics]
Y:598 [binder, in Sierpinski.Basics]
y:602 [binder, in Sierpinski.Basics]
Y:604 [binder, in Sierpinski.Basics]
Y:608 [binder, in Sierpinski.Basics]
Y:612 [binder, in Sierpinski.Basics]
Y:616 [binder, in Sierpinski.Basics]
Y:628 [binder, in Sierpinski.Basics]
Y:638 [binder, in Sierpinski.Basics]
Y:648 [binder, in Sierpinski.Basics]
y:67 [binder, in Sierpinski.Sierpinski]
y:7 [binder, in Sierpinski.Hartogs]
y:70 [binder, in Sierpinski.Cardinality]
y:72 [binder, in Sierpinski.Cardinality]
y:81 [binder, in Sierpinski.Ordinals]
y:84 [binder, in Sierpinski.Basics]
y:88 [binder, in Sierpinski.Ordinals]
y:9 [binder, in Sierpinski.Hartogs]
y:90 [binder, in Sierpinski.Basics]
y:95 [binder, in Sierpinski.Basics]
Z
zero_ordinal [definition, in Sierpinski.Ordinals]z:210 [binder, in Sierpinski.Basics]
z:218 [binder, in Sierpinski.Basics]
z:232 [binder, in Sierpinski.Ordinals]
z:235 [binder, in Sierpinski.Basics]
z:240 [binder, in Sierpinski.Basics]
z:277 [binder, in Sierpinski.Basics]
z:292 [binder, in Sierpinski.Basics]
z:298 [binder, in Sierpinski.Basics]
z:312 [binder, in Sierpinski.Basics]
z:404 [binder, in Sierpinski.Basics]
z:415 [binder, in Sierpinski.Basics]
z:426 [binder, in Sierpinski.Basics]
other
_ ⊊ _ [notation, in Sierpinski.Ordinals]_ ≃ _ [notation, in Sierpinski.Ordinals]
_ > _ [notation, in Sierpinski.Ordinals]
_ < _ [notation, in Sierpinski.Ordinals]
_ ↠ _ [notation, in Sierpinski.Cardinality]
_ ↪ _ [notation, in Sierpinski.Cardinality]
_ ∼ _ [notation, in Sierpinski.Cardinality]
_ ⁻¹ [notation, in Sierpinski.Cardinality]
_ <= _ <= _ [notation, in Sierpinski.Cardinality]
_ <= _ [notation, in Sierpinski.Cardinality]
_ ⊔ _ [notation, in Sierpinski.Basics]
_ × _ [notation, in Sierpinski.Basics]
_ \ _ [notation, in Sierpinski.Basics]
_ ∩ _ [notation, in Sierpinski.Basics]
_ @ _ [notation, in Sierpinski.Basics]
_ ∪ _ [notation, in Sierpinski.Basics]
_ '' _ [notation, in Sierpinski.Basics]
_ ⊈ _ [notation, in Sierpinski.Basics]
_ ⊆ _ [notation, in Sierpinski.Basics]
_ ∉ _ [notation, in Sierpinski.Basics]
_ ∈ _ [notation, in Sierpinski.Basics]
`( _ , _ ) [notation, in Sierpinski.Basics]
`{ _ , .. , _ } [notation, in Sierpinski.Basics]
`{ } [notation, in Sierpinski.Basics]
`{ _ in _ | _ } [notation, in Sierpinski.Basics]
`{ _ | _ in _ , _ } [notation, in Sierpinski.Basics]
`{ _ | _ in _ } [notation, in Sierpinski.Basics]
δ _ : _ , _ [notation, in Sierpinski.Basics]
π1 [notation, in Sierpinski.Basics]
π2 [notation, in Sierpinski.Basics]
∅ [notation, in Sierpinski.Basics]
⋂ _ ∈ _ , _ [notation, in Sierpinski.Basics]
⋃ _ ∈ _ , _ [notation, in Sierpinski.Basics]
𝒫 [notation, in Sierpinski.Basics]
α:138 [binder, in Sierpinski.Ordinals]
α:142 [binder, in Sierpinski.Ordinals]
α:143 [binder, in Sierpinski.Ordinals]
α:147 [binder, in Sierpinski.Ordinals]
α:163 [binder, in Sierpinski.Ordinals]
α:181 [binder, in Sierpinski.Ordinals]
α:184 [binder, in Sierpinski.Ordinals]
α:204 [binder, in Sierpinski.Ordinals]
α:210 [binder, in Sierpinski.Ordinals]
α:212 [binder, in Sierpinski.Ordinals]
α:213 [binder, in Sierpinski.Ordinals]
α:221 [binder, in Sierpinski.Ordinals]
α:224 [binder, in Sierpinski.Ordinals]
α:226 [binder, in Sierpinski.Ordinals]
α:227 [binder, in Sierpinski.Ordinals]
α:68 [binder, in Sierpinski.Sierpinski]
α:69 [binder, in Sierpinski.Sierpinski]
β:148 [binder, in Sierpinski.Ordinals]
β:185 [binder, in Sierpinski.Ordinals]
β:205 [binder, in Sierpinski.Ordinals]
β:211 [binder, in Sierpinski.Ordinals]
β:222 [binder, in Sierpinski.Ordinals]
λ:225 [binder, in Sierpinski.Ordinals]
ξ:159 [binder, in Sierpinski.Ordinals]
ξ:160 [binder, in Sierpinski.Ordinals]
ξ:161 [binder, in Sierpinski.Ordinals]
ξ:162 [binder, in Sierpinski.Ordinals]
ξ:191 [binder, in Sierpinski.Ordinals]
σ [abbreviation, in Sierpinski.Basics]
Notation Index
other
_ ⊊ _ [in Sierpinski.Ordinals]_ ≃ _ [in Sierpinski.Ordinals]
_ > _ [in Sierpinski.Ordinals]
_ < _ [in Sierpinski.Ordinals]
_ ↠ _ [in Sierpinski.Cardinality]
_ ↪ _ [in Sierpinski.Cardinality]
_ ∼ _ [in Sierpinski.Cardinality]
_ ⁻¹ [in Sierpinski.Cardinality]
_ <= _ <= _ [in Sierpinski.Cardinality]
_ <= _ [in Sierpinski.Cardinality]
_ ⊔ _ [in Sierpinski.Basics]
_ × _ [in Sierpinski.Basics]
_ \ _ [in Sierpinski.Basics]
_ ∩ _ [in Sierpinski.Basics]
_ @ _ [in Sierpinski.Basics]
_ ∪ _ [in Sierpinski.Basics]
_ '' _ [in Sierpinski.Basics]
_ ⊈ _ [in Sierpinski.Basics]
_ ⊆ _ [in Sierpinski.Basics]
_ ∉ _ [in Sierpinski.Basics]
_ ∈ _ [in Sierpinski.Basics]
`( _ , _ ) [in Sierpinski.Basics]
`{ _ , .. , _ } [in Sierpinski.Basics]
`{ } [in Sierpinski.Basics]
`{ _ in _ | _ } [in Sierpinski.Basics]
`{ _ | _ in _ , _ } [in Sierpinski.Basics]
`{ _ | _ in _ } [in Sierpinski.Basics]
δ _ : _ , _ [in Sierpinski.Basics]
π1 [in Sierpinski.Basics]
π2 [in Sierpinski.Basics]
∅ [in Sierpinski.Basics]
⋂ _ ∈ _ , _ [in Sierpinski.Basics]
⋃ _ ∈ _ , _ [in Sierpinski.Basics]
𝒫 [in Sierpinski.Basics]
Binder Index
A
A':104 [in Sierpinski.Basics]A':109 [in Sierpinski.Basics]
A':114 [in Sierpinski.Basics]
A':122 [in Sierpinski.Basics]
A':124 [in Sierpinski.Basics]
a':168 [in Sierpinski.Ordinals]
A':168 [in Sierpinski.Cardinality]
A':172 [in Sierpinski.Cardinality]
a':200 [in Sierpinski.Basics]
A':230 [in Sierpinski.Ordinals]
A':238 [in Sierpinski.Ordinals]
a':445 [in Sierpinski.Basics]
A':58 [in Sierpinski.Ordinals]
a':60 [in Sierpinski.Ordinals]
a':63 [in Sierpinski.Ordinals]
a':66 [in Sierpinski.Ordinals]
a':67 [in Sierpinski.Ordinals]
a':68 [in Sierpinski.Ordinals]
A':71 [in Sierpinski.Ordinals]
a':73 [in Sierpinski.Ordinals]
A':73 [in Sierpinski.Basics]
a':75 [in Sierpinski.Ordinals]
a1:104 [in Sierpinski.Ordinals]
a1:13 [in Sierpinski.Ordinals]
a1:23 [in Sierpinski.Ordinals]
a1:4 [in Sierpinski.Ordinals]
a1:40 [in Sierpinski.Ordinals]
A1:56 [in Sierpinski.Sierpinski]
A1:58 [in Sierpinski.Sierpinski]
A1:60 [in Sierpinski.Sierpinski]
A1:62 [in Sierpinski.Sierpinski]
A1:76 [in Sierpinski.Basics]
a1:9 [in Sierpinski.Ordinals]
a2:10 [in Sierpinski.Ordinals]
a2:105 [in Sierpinski.Ordinals]
a2:14 [in Sierpinski.Ordinals]
a2:24 [in Sierpinski.Ordinals]
a2:41 [in Sierpinski.Ordinals]
a2:5 [in Sierpinski.Ordinals]
A2:57 [in Sierpinski.Sierpinski]
A2:59 [in Sierpinski.Sierpinski]
A2:64 [in Sierpinski.Sierpinski]
A2:65 [in Sierpinski.Sierpinski]
A2:77 [in Sierpinski.Basics]
A:1 [in Sierpinski.Ordinals]
A:1 [in Sierpinski.Cardinality]
A:1 [in Sierpinski.Sierpinski]
A:1 [in Sierpinski.Hartogs]
A:10 [in Sierpinski.Hartogs]
a:100 [in Sierpinski.Basics]
a:101 [in Sierpinski.Cardinality]
A:101 [in Sierpinski.Basics]
a:104 [in Sierpinski.Cardinality]
a:105 [in Sierpinski.Basics]
A:106 [in Sierpinski.Ordinals]
A:106 [in Sierpinski.Basics]
a:107 [in Sierpinski.Cardinality]
A:108 [in Sierpinski.Cardinality]
A:11 [in Sierpinski.Ordinals]
a:11 [in Sierpinski.Cardinality]
A:11 [in Sierpinski.Hartogs]
A:110 [in Sierpinski.Cardinality]
A:111 [in Sierpinski.Ordinals]
A:112 [in Sierpinski.Basics]
A:114 [in Sierpinski.Cardinality]
A:116 [in Sierpinski.Cardinality]
A:117 [in Sierpinski.Basics]
A:119 [in Sierpinski.Ordinals]
A:119 [in Sierpinski.Cardinality]
A:12 [in Sierpinski.Hartogs]
A:123 [in Sierpinski.Ordinals]
A:123 [in Sierpinski.Basics]
A:125 [in Sierpinski.Ordinals]
A:125 [in Sierpinski.Basics]
a:128 [in Sierpinski.Basics]
A:129 [in Sierpinski.Basics]
A:13 [in Sierpinski.Hartogs]
A:131 [in Sierpinski.Ordinals]
a:132 [in Sierpinski.Basics]
A:133 [in Sierpinski.Basics]
A:135 [in Sierpinski.Ordinals]
A:14 [in Sierpinski.Basics]
A:141 [in Sierpinski.Cardinality]
A:143 [in Sierpinski.Cardinality]
A:143 [in Sierpinski.Basics]
A:146 [in Sierpinski.Cardinality]
a:149 [in Sierpinski.Cardinality]
A:15 [in Sierpinski.Ordinals]
A:15 [in Sierpinski.Cardinality]
a:152 [in Sierpinski.Cardinality]
A:156 [in Sierpinski.Cardinality]
A:157 [in Sierpinski.Cardinality]
A:16 [in Sierpinski.Cardinality]
A:162 [in Sierpinski.Cardinality]
A:162 [in Sierpinski.Basics]
a:163 [in Sierpinski.Cardinality]
A:164 [in Sierpinski.Ordinals]
a:164 [in Sierpinski.Cardinality]
a:165 [in Sierpinski.Cardinality]
a:166 [in Sierpinski.Cardinality]
a:167 [in Sierpinski.Ordinals]
A:167 [in Sierpinski.Cardinality]
a:169 [in Sierpinski.Ordinals]
A:169 [in Sierpinski.Basics]
A:170 [in Sierpinski.Ordinals]
A:170 [in Sierpinski.Cardinality]
A:172 [in Sierpinski.Ordinals]
A:173 [in Sierpinski.Basics]
A:174 [in Sierpinski.Ordinals]
A:174 [in Sierpinski.Cardinality]
A:176 [in Sierpinski.Basics]
A:177 [in Sierpinski.Cardinality]
a:178 [in Sierpinski.Basics]
A:18 [in Sierpinski.Ordinals]
A:18 [in Sierpinski.Sierpinski]
a:180 [in Sierpinski.Basics]
a:181 [in Sierpinski.Basics]
A:182 [in Sierpinski.Basics]
A:183 [in Sierpinski.Cardinality]
A:188 [in Sierpinski.Basics]
A:19 [in Sierpinski.Cardinality]
A:19 [in Sierpinski.Basics]
A:191 [in Sierpinski.Basics]
A:194 [in Sierpinski.Basics]
a:198 [in Sierpinski.Basics]
a:199 [in Sierpinski.Basics]
a:206 [in Sierpinski.Basics]
A:21 [in Sierpinski.Ordinals]
A:21 [in Sierpinski.Sierpinski]
A:220 [in Sierpinski.Basics]
A:223 [in Sierpinski.Basics]
A:225 [in Sierpinski.Basics]
A:228 [in Sierpinski.Ordinals]
A:228 [in Sierpinski.Basics]
A:229 [in Sierpinski.Ordinals]
A:23 [in Sierpinski.Cardinality]
A:233 [in Sierpinski.Ordinals]
A:237 [in Sierpinski.Ordinals]
A:240 [in Sierpinski.Ordinals]
A:246 [in Sierpinski.Ordinals]
A:25 [in Sierpinski.Ordinals]
A:250 [in Sierpinski.Ordinals]
A:27 [in Sierpinski.Cardinality]
A:271 [in Sierpinski.Basics]
A:275 [in Sierpinski.Basics]
A:28 [in Sierpinski.Ordinals]
A:285 [in Sierpinski.Basics]
a:287 [in Sierpinski.Basics]
a:288 [in Sierpinski.Basics]
A:289 [in Sierpinski.Basics]
A:29 [in Sierpinski.Basics]
A:295 [in Sierpinski.Basics]
A:3 [in Sierpinski.Hartogs]
A:30 [in Sierpinski.Sierpinski]
A:301 [in Sierpinski.Basics]
A:305 [in Sierpinski.Basics]
A:313 [in Sierpinski.Basics]
a:314 [in Sierpinski.Basics]
A:32 [in Sierpinski.Cardinality]
A:320 [in Sierpinski.Basics]
A:34 [in Sierpinski.Ordinals]
A:348 [in Sierpinski.Basics]
A:35 [in Sierpinski.Cardinality]
A:35 [in Sierpinski.Basics]
a:352 [in Sierpinski.Basics]
A:354 [in Sierpinski.Basics]
a:358 [in Sierpinski.Basics]
A:359 [in Sierpinski.Basics]
A:36 [in Sierpinski.Ordinals]
A:363 [in Sierpinski.Basics]
A:366 [in Sierpinski.Basics]
A:38 [in Sierpinski.Ordinals]
A:38 [in Sierpinski.Cardinality]
A:382 [in Sierpinski.Basics]
A:386 [in Sierpinski.Basics]
A:39 [in Sierpinski.Basics]
A:390 [in Sierpinski.Basics]
A:396 [in Sierpinski.Basics]
A:40 [in Sierpinski.Cardinality]
A:402 [in Sierpinski.Basics]
A:407 [in Sierpinski.Basics]
A:413 [in Sierpinski.Basics]
A:418 [in Sierpinski.Basics]
A:42 [in Sierpinski.Ordinals]
A:42 [in Sierpinski.Cardinality]
A:42 [in Sierpinski.Basics]
A:424 [in Sierpinski.Basics]
a:427 [in Sierpinski.Basics]
a:429 [in Sierpinski.Basics]
A:43 [in Sierpinski.Cardinality]
A:431 [in Sierpinski.Basics]
A:432 [in Sierpinski.Basics]
a:434 [in Sierpinski.Basics]
A:436 [in Sierpinski.Basics]
A:439 [in Sierpinski.Basics]
A:442 [in Sierpinski.Basics]
a:444 [in Sierpinski.Basics]
A:446 [in Sierpinski.Basics]
A:45 [in Sierpinski.Cardinality]
A:450 [in Sierpinski.Basics]
a:452 [in Sierpinski.Basics]
A:454 [in Sierpinski.Basics]
A:46 [in Sierpinski.Basics]
a:461 [in Sierpinski.Basics]
A:463 [in Sierpinski.Basics]
a:470 [in Sierpinski.Basics]
a:472 [in Sierpinski.Basics]
A:474 [in Sierpinski.Basics]
A:48 [in Sierpinski.Cardinality]
A:480 [in Sierpinski.Basics]
a:483 [in Sierpinski.Basics]
A:486 [in Sierpinski.Basics]
A:49 [in Sierpinski.Basics]
A:492 [in Sierpinski.Basics]
a:497 [in Sierpinski.Basics]
A:498 [in Sierpinski.Basics]
A:499 [in Sierpinski.Basics]
A:5 [in Sierpinski.Sierpinski]
a:502 [in Sierpinski.Basics]
A:503 [in Sierpinski.Basics]
a:507 [in Sierpinski.Basics]
a:508 [in Sierpinski.Basics]
A:509 [in Sierpinski.Basics]
A:513 [in Sierpinski.Basics]
A:517 [in Sierpinski.Basics]
A:523 [in Sierpinski.Basics]
A:529 [in Sierpinski.Basics]
A:53 [in Sierpinski.Cardinality]
A:53 [in Sierpinski.Basics]
A:54 [in Sierpinski.Cardinality]
A:54 [in Sierpinski.Sierpinski]
A:543 [in Sierpinski.Basics]
A:56 [in Sierpinski.Ordinals]
A:564 [in Sierpinski.Basics]
A:574 [in Sierpinski.Basics]
a:583 [in Sierpinski.Basics]
a:585 [in Sierpinski.Basics]
a:587 [in Sierpinski.Basics]
a:589 [in Sierpinski.Basics]
a:59 [in Sierpinski.Ordinals]
A:59 [in Sierpinski.Cardinality]
a:591 [in Sierpinski.Basics]
a:593 [in Sierpinski.Basics]
A:6 [in Sierpinski.Ordinals]
A:6 [in Sierpinski.Cardinality]
a:61 [in Sierpinski.Ordinals]
a:61 [in Sierpinski.Sierpinski]
a:62 [in Sierpinski.Ordinals]
A:62 [in Sierpinski.Cardinality]
A:620 [in Sierpinski.Basics]
A:622 [in Sierpinski.Basics]
a:625 [in Sierpinski.Basics]
A:629 [in Sierpinski.Basics]
a:63 [in Sierpinski.Sierpinski]
a:64 [in Sierpinski.Ordinals]
A:64 [in Sierpinski.Basics]
a:65 [in Sierpinski.Ordinals]
A:65 [in Sierpinski.Cardinality]
A:68 [in Sierpinski.Basics]
A:69 [in Sierpinski.Ordinals]
A:7 [in Sierpinski.Basics]
a:72 [in Sierpinski.Ordinals]
A:72 [in Sierpinski.Basics]
a:74 [in Sierpinski.Ordinals]
A:74 [in Sierpinski.Cardinality]
A:75 [in Sierpinski.Basics]
A:76 [in Sierpinski.Ordinals]
A:76 [in Sierpinski.Cardinality]
A:78 [in Sierpinski.Cardinality]
a:78 [in Sierpinski.Basics]
A:79 [in Sierpinski.Cardinality]
A:82 [in Sierpinski.Ordinals]
A:82 [in Sierpinski.Cardinality]
A:83 [in Sierpinski.Basics]
A:85 [in Sierpinski.Cardinality]
A:87 [in Sierpinski.Basics]
A:89 [in Sierpinski.Ordinals]
A:90 [in Sierpinski.Cardinality]
a:91 [in Sierpinski.Cardinality]
a:92 [in Sierpinski.Cardinality]
A:93 [in Sierpinski.Cardinality]
A:93 [in Sierpinski.Basics]
A:94 [in Sierpinski.Ordinals]
A:97 [in Sierpinski.Basics]
a:98 [in Sierpinski.Cardinality]
A:99 [in Sierpinski.Ordinals]
B
base:349 [in Sierpinski.Basics]base:355 [in Sierpinski.Basics]
base:360 [in Sierpinski.Basics]
base:365 [in Sierpinski.Basics]
base:369 [in Sierpinski.Basics]
b':449 [in Sierpinski.Basics]
b1:244 [in Sierpinski.Ordinals]
b2:245 [in Sierpinski.Ordinals]
b:100 [in Sierpinski.Cardinality]
B:101 [in Sierpinski.Ordinals]
B:102 [in Sierpinski.Basics]
b:103 [in Sierpinski.Cardinality]
b:106 [in Sierpinski.Cardinality]
B:107 [in Sierpinski.Basics]
B:108 [in Sierpinski.Ordinals]
B:109 [in Sierpinski.Cardinality]
B:111 [in Sierpinski.Cardinality]
B:112 [in Sierpinski.Ordinals]
B:113 [in Sierpinski.Basics]
B:115 [in Sierpinski.Cardinality]
B:117 [in Sierpinski.Cardinality]
B:118 [in Sierpinski.Basics]
B:120 [in Sierpinski.Cardinality]
B:121 [in Sierpinski.Ordinals]
B:126 [in Sierpinski.Basics]
B:127 [in Sierpinski.Ordinals]
b:13 [in Sierpinski.Cardinality]
B:130 [in Sierpinski.Basics]
B:133 [in Sierpinski.Ordinals]
B:142 [in Sierpinski.Cardinality]
B:147 [in Sierpinski.Cardinality]
b:150 [in Sierpinski.Cardinality]
b:153 [in Sierpinski.Cardinality]
B:158 [in Sierpinski.Cardinality]
B:17 [in Sierpinski.Cardinality]
B:184 [in Sierpinski.Cardinality]
B:20 [in Sierpinski.Cardinality]
b:207 [in Sierpinski.Basics]
B:221 [in Sierpinski.Basics]
B:224 [in Sierpinski.Basics]
B:226 [in Sierpinski.Basics]
B:229 [in Sierpinski.Basics]
B:24 [in Sierpinski.Cardinality]
B:241 [in Sierpinski.Ordinals]
B:247 [in Sierpinski.Ordinals]
B:251 [in Sierpinski.Ordinals]
B:28 [in Sierpinski.Cardinality]
B:280 [in Sierpinski.Basics]
B:282 [in Sierpinski.Basics]
B:302 [in Sierpinski.Basics]
B:306 [in Sierpinski.Basics]
B:33 [in Sierpinski.Cardinality]
B:36 [in Sierpinski.Cardinality]
B:383 [in Sierpinski.Basics]
B:387 [in Sierpinski.Basics]
B:39 [in Sierpinski.Cardinality]
B:391 [in Sierpinski.Basics]
B:397 [in Sierpinski.Basics]
B:403 [in Sierpinski.Basics]
B:408 [in Sierpinski.Basics]
B:41 [in Sierpinski.Cardinality]
B:414 [in Sierpinski.Basics]
B:419 [in Sierpinski.Basics]
B:425 [in Sierpinski.Basics]
b:428 [in Sierpinski.Basics]
B:43 [in Sierpinski.Basics]
b:430 [in Sierpinski.Basics]
B:433 [in Sierpinski.Basics]
b:435 [in Sierpinski.Basics]
B:437 [in Sierpinski.Basics]
B:44 [in Sierpinski.Cardinality]
B:440 [in Sierpinski.Basics]
B:443 [in Sierpinski.Basics]
B:447 [in Sierpinski.Basics]
b:448 [in Sierpinski.Basics]
B:451 [in Sierpinski.Basics]
b:453 [in Sierpinski.Basics]
B:455 [in Sierpinski.Basics]
B:46 [in Sierpinski.Cardinality]
b:462 [in Sierpinski.Basics]
B:464 [in Sierpinski.Basics]
b:471 [in Sierpinski.Basics]
b:473 [in Sierpinski.Basics]
B:475 [in Sierpinski.Basics]
B:481 [in Sierpinski.Basics]
B:487 [in Sierpinski.Basics]
b:489 [in Sierpinski.Basics]
B:49 [in Sierpinski.Cardinality]
B:493 [in Sierpinski.Basics]
b:496 [in Sierpinski.Basics]
B:50 [in Sierpinski.Basics]
B:500 [in Sierpinski.Basics]
B:504 [in Sierpinski.Basics]
B:510 [in Sierpinski.Basics]
B:514 [in Sierpinski.Basics]
b:516 [in Sierpinski.Basics]
B:518 [in Sierpinski.Basics]
b:521 [in Sierpinski.Basics]
b:522 [in Sierpinski.Basics]
B:524 [in Sierpinski.Basics]
B:530 [in Sierpinski.Basics]
B:54 [in Sierpinski.Basics]
B:55 [in Sierpinski.Cardinality]
B:55 [in Sierpinski.Sierpinski]
B:565 [in Sierpinski.Basics]
B:575 [in Sierpinski.Basics]
B:6 [in Sierpinski.Sierpinski]
B:60 [in Sierpinski.Cardinality]
B:623 [in Sierpinski.Basics]
b:626 [in Sierpinski.Basics]
B:63 [in Sierpinski.Cardinality]
B:630 [in Sierpinski.Basics]
b:639 [in Sierpinski.Basics]
b:640 [in Sierpinski.Basics]
b:643 [in Sierpinski.Basics]
b:644 [in Sierpinski.Basics]
b:645 [in Sierpinski.Basics]
b:646 [in Sierpinski.Basics]
B:65 [in Sierpinski.Basics]
B:66 [in Sierpinski.Cardinality]
B:69 [in Sierpinski.Basics]
B:7 [in Sierpinski.Cardinality]
B:75 [in Sierpinski.Cardinality]
B:77 [in Sierpinski.Cardinality]
B:78 [in Sierpinski.Ordinals]
B:80 [in Sierpinski.Cardinality]
B:83 [in Sierpinski.Cardinality]
B:84 [in Sierpinski.Ordinals]
B:91 [in Sierpinski.Ordinals]
B:94 [in Sierpinski.Cardinality]
B:96 [in Sierpinski.Ordinals]
b:97 [in Sierpinski.Cardinality]
B:98 [in Sierpinski.Basics]
C
c:102 [in Sierpinski.Cardinality]c:105 [in Sierpinski.Cardinality]
C:113 [in Sierpinski.Ordinals]
C:119 [in Sierpinski.Basics]
C:129 [in Sierpinski.Ordinals]
C:29 [in Sierpinski.Cardinality]
C:303 [in Sierpinski.Basics]
C:456 [in Sierpinski.Basics]
c:460 [in Sierpinski.Basics]
C:465 [in Sierpinski.Basics]
c:469 [in Sierpinski.Basics]
C:47 [in Sierpinski.Cardinality]
C:476 [in Sierpinski.Basics]
C:482 [in Sierpinski.Basics]
C:488 [in Sierpinski.Basics]
c:554 [in Sierpinski.Basics]
c:557 [in Sierpinski.Basics]
C:56 [in Sierpinski.Cardinality]
c:569 [in Sierpinski.Basics]
C:81 [in Sierpinski.Cardinality]
C:95 [in Sierpinski.Cardinality]
c:96 [in Sierpinski.Cardinality]
c:99 [in Sierpinski.Cardinality]
E
elements1:257 [in Sierpinski.Basics]elements1:261 [in Sierpinski.Basics]
elements2:258 [in Sierpinski.Basics]
elements2:262 [in Sierpinski.Basics]
elements:241 [in Sierpinski.Basics]
elements:244 [in Sierpinski.Basics]
elements:249 [in Sierpinski.Basics]
elements:254 [in Sierpinski.Basics]
F
f1:117 [in Sierpinski.Ordinals]f1:30 [in Sierpinski.Cardinality]
f2:118 [in Sierpinski.Ordinals]
f2:31 [in Sierpinski.Cardinality]
f:103 [in Sierpinski.Ordinals]
f:103 [in Sierpinski.Basics]
f:108 [in Sierpinski.Basics]
f:110 [in Sierpinski.Ordinals]
f:115 [in Sierpinski.Basics]
f:120 [in Sierpinski.Basics]
f:127 [in Sierpinski.Basics]
F:13 [in Sierpinski.Sierpinski]
f:131 [in Sierpinski.Basics]
f:136 [in Sierpinski.Basics]
f:146 [in Sierpinski.Basics]
f:18 [in Sierpinski.Cardinality]
f:190 [in Sierpinski.Ordinals]
f:21 [in Sierpinski.Cardinality]
F:215 [in Sierpinski.Ordinals]
F:219 [in Sierpinski.Ordinals]
f:242 [in Sierpinski.Ordinals]
f:248 [in Sierpinski.Ordinals]
f:25 [in Sierpinski.Cardinality]
f:252 [in Sierpinski.Ordinals]
f:272 [in Sierpinski.Basics]
f:276 [in Sierpinski.Basics]
f:286 [in Sierpinski.Basics]
f:290 [in Sierpinski.Basics]
f:296 [in Sierpinski.Basics]
f:31 [in Sierpinski.Sierpinski]
f:34 [in Sierpinski.Cardinality]
f:37 [in Sierpinski.Cardinality]
f:534 [in Sierpinski.Basics]
f:539 [in Sierpinski.Basics]
f:544 [in Sierpinski.Basics]
f:566 [in Sierpinski.Basics]
f:57 [in Sierpinski.Cardinality]
f:576 [in Sierpinski.Basics]
f:599 [in Sierpinski.Basics]
f:605 [in Sierpinski.Basics]
f:609 [in Sierpinski.Basics]
f:61 [in Sierpinski.Cardinality]
f:613 [in Sierpinski.Basics]
f:617 [in Sierpinski.Basics]
f:624 [in Sierpinski.Basics]
f:631 [in Sierpinski.Basics]
f:64 [in Sierpinski.Cardinality]
f:67 [in Sierpinski.Cardinality]
f:8 [in Sierpinski.Sierpinski]
f:84 [in Sierpinski.Cardinality]
f:86 [in Sierpinski.Ordinals]
f:88 [in Sierpinski.Basics]
f:93 [in Sierpinski.Ordinals]
f:94 [in Sierpinski.Basics]
f:98 [in Sierpinski.Ordinals]
f:99 [in Sierpinski.Basics]
G
g':633 [in Sierpinski.Basics]g:121 [in Sierpinski.Basics]
g:567 [in Sierpinski.Basics]
g:577 [in Sierpinski.Basics]
g:58 [in Sierpinski.Cardinality]
g:600 [in Sierpinski.Basics]
g:606 [in Sierpinski.Basics]
g:610 [in Sierpinski.Basics]
g:614 [in Sierpinski.Basics]
g:618 [in Sierpinski.Basics]
g:632 [in Sierpinski.Basics]
H
H':528 [in Sierpinski.Basics]h':579 [in Sierpinski.Basics]
H':6 [in Sierpinski.Basics]
H0:146 [in Sierpinski.Ordinals]
H:123 [in Sierpinski.Cardinality]
H:124 [in Sierpinski.Cardinality]
H:127 [in Sierpinski.Cardinality]
H:128 [in Sierpinski.Cardinality]
H:130 [in Sierpinski.Cardinality]
H:131 [in Sierpinski.Cardinality]
H:133 [in Sierpinski.Cardinality]
H:134 [in Sierpinski.Cardinality]
H:139 [in Sierpinski.Basics]
H:144 [in Sierpinski.Ordinals]
H:167 [in Sierpinski.Basics]
H:17 [in Sierpinski.Ordinals]
H:171 [in Sierpinski.Cardinality]
H:172 [in Sierpinski.Basics]
H:175 [in Sierpinski.Cardinality]
H:178 [in Sierpinski.Cardinality]
H:193 [in Sierpinski.Basics]
H:20 [in Sierpinski.Ordinals]
H:27 [in Sierpinski.Ordinals]
H:3 [in Sierpinski.Ordinals]
H:3 [in Sierpinski.Cardinality]
H:325 [in Sierpinski.Basics]
H:48 [in Sierpinski.Basics]
H:5 [in Sierpinski.Basics]
H:506 [in Sierpinski.Basics]
H:520 [in Sierpinski.Basics]
H:527 [in Sierpinski.Basics]
h:568 [in Sierpinski.Basics]
h:578 [in Sierpinski.Basics]
h:634 [in Sierpinski.Basics]
H:79 [in Sierpinski.Ordinals]
H:8 [in Sierpinski.Ordinals]
H:82 [in Sierpinski.Basics]
H:91 [in Sierpinski.Basics]
I
Is_From_Left0:512 [in Sierpinski.Basics]I:12 [in Sierpinski.Sierpinski]
i:14 [in Sierpinski.Sierpinski]
i:15 [in Sierpinski.Sierpinski]
i:16 [in Sierpinski.Sierpinski]
i:17 [in Sierpinski.Sierpinski]
i:19 [in Sierpinski.Sierpinski]
i:20 [in Sierpinski.Sierpinski]
I:214 [in Sierpinski.Ordinals]
i:216 [in Sierpinski.Ordinals]
i:217 [in Sierpinski.Ordinals]
I:218 [in Sierpinski.Ordinals]
i:22 [in Sierpinski.Sierpinski]
i:220 [in Sierpinski.Ordinals]
i:23 [in Sierpinski.Sierpinski]
i:38 [in Sierpinski.Sierpinski]
i:39 [in Sierpinski.Sierpinski]
i:40 [in Sierpinski.Sierpinski]
i:42 [in Sierpinski.Sierpinski]
i:44 [in Sierpinski.Sierpinski]
i:45 [in Sierpinski.Sierpinski]
i:46 [in Sierpinski.Sierpinski]
i:47 [in Sierpinski.Sierpinski]
i:48 [in Sierpinski.Sierpinski]
i:49 [in Sierpinski.Sierpinski]
i:50 [in Sierpinski.Sierpinski]
i:51 [in Sierpinski.Sierpinski]
i:52 [in Sierpinski.Sierpinski]
i:53 [in Sierpinski.Sierpinski]
L
l_step:490 [in Sierpinski.Basics]l_step:484 [in Sierpinski.Basics]
l_step:477 [in Sierpinski.Basics]
l_step:466 [in Sierpinski.Basics]
l_step:457 [in Sierpinski.Basics]
l:15 [in Sierpinski.Basics]
l:20 [in Sierpinski.Basics]
N
n':342 [in Sierpinski.Basics]n':344 [in Sierpinski.Basics]
n0:353 [in Sierpinski.Basics]
n:112 [in Sierpinski.Cardinality]
n:113 [in Sierpinski.Cardinality]
n:327 [in Sierpinski.Basics]
n:332 [in Sierpinski.Basics]
n:334 [in Sierpinski.Basics]
n:335 [in Sierpinski.Basics]
n:338 [in Sierpinski.Basics]
n:340 [in Sierpinski.Basics]
n:341 [in Sierpinski.Basics]
n:343 [in Sierpinski.Basics]
n:346 [in Sierpinski.Basics]
n:347 [in Sierpinski.Basics]
n:351 [in Sierpinski.Basics]
n:357 [in Sierpinski.Basics]
n:362 [in Sierpinski.Basics]
n:367 [in Sierpinski.Basics]
n:70 [in Sierpinski.Sierpinski]
n:71 [in Sierpinski.Sierpinski]
n:72 [in Sierpinski.Sierpinski]
n:73 [in Sierpinski.Sierpinski]
P
P_x:161 [in Sierpinski.Basics]P_x:159 [in Sierpinski.Basics]
P_x:155 [in Sierpinski.Basics]
P_x:153 [in Sierpinski.Basics]
P_x:149 [in Sierpinski.Basics]
P_x:140 [in Sierpinski.Basics]
P:1 [in Sierpinski.Basics]
P:134 [in Sierpinski.Basics]
P:144 [in Sierpinski.Basics]
P:16 [in Sierpinski.Basics]
P:164 [in Sierpinski.Basics]
P:166 [in Sierpinski.Ordinals]
P:170 [in Sierpinski.Basics]
P:174 [in Sierpinski.Basics]
P:177 [in Sierpinski.Basics]
P:196 [in Sierpinski.Basics]
P:21 [in Sierpinski.Basics]
P:223 [in Sierpinski.Ordinals]
P:245 [in Sierpinski.Basics]
P:250 [in Sierpinski.Basics]
P:315 [in Sierpinski.Basics]
P:321 [in Sierpinski.Basics]
P:345 [in Sierpinski.Basics]
P:370 [in Sierpinski.Basics]
P:4 [in Sierpinski.Basics]
P:44 [in Sierpinski.Ordinals]
P:494 [in Sierpinski.Basics]
P:545 [in Sierpinski.Basics]
P:547 [in Sierpinski.Basics]
P:60 [in Sierpinski.Basics]
Q
Q:2 [in Sierpinski.Basics]R
R__B:134 [in Sierpinski.Ordinals]R__A:132 [in Sierpinski.Ordinals]
R__C:130 [in Sierpinski.Ordinals]
R__B:128 [in Sierpinski.Ordinals]
R__A:126 [in Sierpinski.Ordinals]
R__C:116 [in Sierpinski.Ordinals]
R__B:115 [in Sierpinski.Ordinals]
R__A:114 [in Sierpinski.Ordinals]
r_step:491 [in Sierpinski.Basics]
r_step:485 [in Sierpinski.Basics]
r_step:478 [in Sierpinski.Basics]
r_step:467 [in Sierpinski.Basics]
r_step:458 [in Sierpinski.Basics]
R':102 [in Sierpinski.Ordinals]
R':109 [in Sierpinski.Ordinals]
R':122 [in Sierpinski.Ordinals]
R':85 [in Sierpinski.Ordinals]
R':92 [in Sierpinski.Ordinals]
R':97 [in Sierpinski.Ordinals]
R:100 [in Sierpinski.Ordinals]
R:107 [in Sierpinski.Ordinals]
R:12 [in Sierpinski.Ordinals]
R:120 [in Sierpinski.Ordinals]
R:124 [in Sierpinski.Ordinals]
R:16 [in Sierpinski.Ordinals]
R:165 [in Sierpinski.Ordinals]
R:171 [in Sierpinski.Ordinals]
R:173 [in Sierpinski.Ordinals]
R:183 [in Sierpinski.Basics]
R:189 [in Sierpinski.Basics]
R:19 [in Sierpinski.Ordinals]
R:192 [in Sierpinski.Basics]
R:195 [in Sierpinski.Basics]
R:2 [in Sierpinski.Ordinals]
R:2 [in Sierpinski.Cardinality]
R:22 [in Sierpinski.Ordinals]
R:231 [in Sierpinski.Ordinals]
R:234 [in Sierpinski.Ordinals]
R:239 [in Sierpinski.Ordinals]
R:243 [in Sierpinski.Ordinals]
R:249 [in Sierpinski.Ordinals]
R:253 [in Sierpinski.Ordinals]
R:26 [in Sierpinski.Ordinals]
R:35 [in Sierpinski.Ordinals]
R:37 [in Sierpinski.Ordinals]
R:39 [in Sierpinski.Ordinals]
R:43 [in Sierpinski.Ordinals]
R:57 [in Sierpinski.Ordinals]
R:7 [in Sierpinski.Ordinals]
R:7 [in Sierpinski.Sierpinski]
R:70 [in Sierpinski.Ordinals]
R:77 [in Sierpinski.Ordinals]
R:79 [in Sierpinski.Basics]
R:8 [in Sierpinski.Basics]
R:81 [in Sierpinski.Basics]
R:83 [in Sierpinski.Ordinals]
R:90 [in Sierpinski.Ordinals]
R:95 [in Sierpinski.Ordinals]
S
step:350 [in Sierpinski.Basics]step:356 [in Sierpinski.Basics]
step:361 [in Sierpinski.Basics]
step:364 [in Sierpinski.Basics]
step:368 [in Sierpinski.Basics]
U
u:269 [in Sierpinski.Basics]u:309 [in Sierpinski.Basics]
V
v:270 [in Sierpinski.Basics]W
wf:197 [in Sierpinski.Basics]X
x_in_A:157 [in Sierpinski.Basics]x_in_A:151 [in Sierpinski.Basics]
x_in_B:45 [in Sierpinski.Basics]
x':152 [in Sierpinski.Basics]
x':158 [in Sierpinski.Basics]
x':375 [in Sierpinski.Basics]
x':379 [in Sierpinski.Basics]
x':393 [in Sierpinski.Basics]
x':399 [in Sierpinski.Basics]
x':422 [in Sierpinski.Basics]
x':423 [in Sierpinski.Basics]
x':526 [in Sierpinski.Basics]
x':536 [in Sierpinski.Basics]
x0:48 [in Sierpinski.Ordinals]
x0:51 [in Sierpinski.Ordinals]
x0:636 [in Sierpinski.Basics]
x0:641 [in Sierpinski.Basics]
x0:642 [in Sierpinski.Basics]
x:10 [in Sierpinski.Sierpinski]
x:10 [in Sierpinski.Basics]
x:111 [in Sierpinski.Basics]
x:116 [in Sierpinski.Basics]
x:118 [in Sierpinski.Cardinality]
x:121 [in Sierpinski.Cardinality]
x:125 [in Sierpinski.Cardinality]
x:129 [in Sierpinski.Cardinality]
x:132 [in Sierpinski.Cardinality]
x:135 [in Sierpinski.Cardinality]
x:135 [in Sierpinski.Basics]
x:136 [in Sierpinski.Ordinals]
x:136 [in Sierpinski.Cardinality]
x:137 [in Sierpinski.Cardinality]
x:137 [in Sierpinski.Basics]
x:138 [in Sierpinski.Cardinality]
x:139 [in Sierpinski.Cardinality]
x:140 [in Sierpinski.Cardinality]
x:141 [in Sierpinski.Ordinals]
x:141 [in Sierpinski.Basics]
x:142 [in Sierpinski.Basics]
x:145 [in Sierpinski.Ordinals]
x:145 [in Sierpinski.Basics]
x:148 [in Sierpinski.Cardinality]
x:148 [in Sierpinski.Basics]
x:149 [in Sierpinski.Ordinals]
x:150 [in Sierpinski.Basics]
x:151 [in Sierpinski.Ordinals]
x:151 [in Sierpinski.Cardinality]
x:153 [in Sierpinski.Ordinals]
x:154 [in Sierpinski.Cardinality]
x:154 [in Sierpinski.Basics]
x:155 [in Sierpinski.Ordinals]
x:155 [in Sierpinski.Cardinality]
x:156 [in Sierpinski.Basics]
x:157 [in Sierpinski.Ordinals]
x:160 [in Sierpinski.Basics]
x:163 [in Sierpinski.Basics]
x:165 [in Sierpinski.Basics]
x:168 [in Sierpinski.Basics]
x:169 [in Sierpinski.Cardinality]
x:171 [in Sierpinski.Basics]
x:173 [in Sierpinski.Cardinality]
x:175 [in Sierpinski.Ordinals]
x:175 [in Sierpinski.Basics]
x:176 [in Sierpinski.Cardinality]
x:177 [in Sierpinski.Ordinals]
x:179 [in Sierpinski.Ordinals]
x:179 [in Sierpinski.Cardinality]
x:179 [in Sierpinski.Basics]
x:180 [in Sierpinski.Cardinality]
x:181 [in Sierpinski.Cardinality]
x:182 [in Sierpinski.Ordinals]
x:182 [in Sierpinski.Cardinality]
x:184 [in Sierpinski.Basics]
x:186 [in Sierpinski.Ordinals]
x:186 [in Sierpinski.Cardinality]
x:188 [in Sierpinski.Ordinals]
x:188 [in Sierpinski.Cardinality]
x:189 [in Sierpinski.Cardinality]
x:190 [in Sierpinski.Basics]
x:191 [in Sierpinski.Cardinality]
x:192 [in Sierpinski.Ordinals]
x:193 [in Sierpinski.Cardinality]
x:194 [in Sierpinski.Ordinals]
x:194 [in Sierpinski.Cardinality]
x:196 [in Sierpinski.Ordinals]
x:197 [in Sierpinski.Ordinals]
x:2 [in Sierpinski.Sierpinski]
x:2 [in Sierpinski.Hartogs]
x:201 [in Sierpinski.Ordinals]
x:202 [in Sierpinski.Basics]
x:203 [in Sierpinski.Ordinals]
x:203 [in Sierpinski.Basics]
x:204 [in Sierpinski.Basics]
x:206 [in Sierpinski.Ordinals]
x:208 [in Sierpinski.Ordinals]
x:208 [in Sierpinski.Basics]
x:211 [in Sierpinski.Basics]
x:212 [in Sierpinski.Basics]
x:214 [in Sierpinski.Basics]
x:216 [in Sierpinski.Basics]
x:219 [in Sierpinski.Basics]
x:22 [in Sierpinski.Cardinality]
x:222 [in Sierpinski.Basics]
x:227 [in Sierpinski.Basics]
x:230 [in Sierpinski.Basics]
x:231 [in Sierpinski.Basics]
x:233 [in Sierpinski.Basics]
x:235 [in Sierpinski.Ordinals]
x:236 [in Sierpinski.Basics]
x:238 [in Sierpinski.Basics]
x:24 [in Sierpinski.Sierpinski]
x:246 [in Sierpinski.Basics]
x:247 [in Sierpinski.Basics]
x:248 [in Sierpinski.Basics]
x:251 [in Sierpinski.Basics]
x:252 [in Sierpinski.Basics]
x:253 [in Sierpinski.Basics]
x:255 [in Sierpinski.Basics]
x:259 [in Sierpinski.Basics]
x:26 [in Sierpinski.Cardinality]
x:26 [in Sierpinski.Sierpinski]
x:263 [in Sierpinski.Basics]
x:265 [in Sierpinski.Basics]
x:267 [in Sierpinski.Basics]
x:273 [in Sierpinski.Basics]
x:274 [in Sierpinski.Basics]
x:278 [in Sierpinski.Basics]
x:279 [in Sierpinski.Basics]
x:28 [in Sierpinski.Sierpinski]
x:28 [in Sierpinski.Basics]
x:281 [in Sierpinski.Basics]
x:283 [in Sierpinski.Basics]
x:284 [in Sierpinski.Basics]
x:29 [in Sierpinski.Sierpinski]
x:291 [in Sierpinski.Basics]
x:293 [in Sierpinski.Basics]
x:294 [in Sierpinski.Basics]
x:297 [in Sierpinski.Basics]
x:299 [in Sierpinski.Basics]
x:300 [in Sierpinski.Basics]
x:304 [in Sierpinski.Basics]
x:307 [in Sierpinski.Basics]
x:310 [in Sierpinski.Basics]
x:318 [in Sierpinski.Basics]
x:32 [in Sierpinski.Sierpinski]
x:32 [in Sierpinski.Basics]
x:322 [in Sierpinski.Basics]
x:323 [in Sierpinski.Basics]
x:326 [in Sierpinski.Basics]
x:33 [in Sierpinski.Sierpinski]
x:33 [in Sierpinski.Basics]
x:331 [in Sierpinski.Basics]
x:339 [in Sierpinski.Basics]
x:34 [in Sierpinski.Sierpinski]
x:35 [in Sierpinski.Sierpinski]
x:36 [in Sierpinski.Sierpinski]
x:37 [in Sierpinski.Sierpinski]
x:371 [in Sierpinski.Basics]
x:372 [in Sierpinski.Basics]
x:374 [in Sierpinski.Basics]
x:378 [in Sierpinski.Basics]
x:384 [in Sierpinski.Basics]
x:388 [in Sierpinski.Basics]
x:392 [in Sierpinski.Basics]
x:398 [in Sierpinski.Basics]
x:4 [in Sierpinski.Cardinality]
x:4 [in Sierpinski.Sierpinski]
x:4 [in Sierpinski.Hartogs]
x:40 [in Sierpinski.Basics]
x:405 [in Sierpinski.Basics]
x:409 [in Sierpinski.Basics]
x:41 [in Sierpinski.Sierpinski]
x:417 [in Sierpinski.Basics]
x:420 [in Sierpinski.Basics]
x:43 [in Sierpinski.Sierpinski]
x:438 [in Sierpinski.Basics]
x:44 [in Sierpinski.Basics]
x:441 [in Sierpinski.Basics]
x:45 [in Sierpinski.Ordinals]
x:459 [in Sierpinski.Basics]
x:468 [in Sierpinski.Basics]
x:47 [in Sierpinski.Ordinals]
x:47 [in Sierpinski.Basics]
x:479 [in Sierpinski.Basics]
x:49 [in Sierpinski.Ordinals]
x:495 [in Sierpinski.Basics]
x:5 [in Sierpinski.Hartogs]
x:501 [in Sierpinski.Basics]
x:505 [in Sierpinski.Basics]
x:51 [in Sierpinski.Basics]
x:511 [in Sierpinski.Basics]
x:515 [in Sierpinski.Basics]
x:519 [in Sierpinski.Basics]
x:52 [in Sierpinski.Ordinals]
x:52 [in Sierpinski.Basics]
x:525 [in Sierpinski.Basics]
x:531 [in Sierpinski.Basics]
X:532 [in Sierpinski.Basics]
x:535 [in Sierpinski.Basics]
X:537 [in Sierpinski.Basics]
x:541 [in Sierpinski.Basics]
X:542 [in Sierpinski.Basics]
x:546 [in Sierpinski.Basics]
x:548 [in Sierpinski.Basics]
x:549 [in Sierpinski.Basics]
x:55 [in Sierpinski.Basics]
x:550 [in Sierpinski.Basics]
x:551 [in Sierpinski.Basics]
X:552 [in Sierpinski.Basics]
x:555 [in Sierpinski.Basics]
x:558 [in Sierpinski.Basics]
X:560 [in Sierpinski.Basics]
X:562 [in Sierpinski.Basics]
x:570 [in Sierpinski.Basics]
X:572 [in Sierpinski.Basics]
x:58 [in Sierpinski.Basics]
X:580 [in Sierpinski.Basics]
X:582 [in Sierpinski.Basics]
x:584 [in Sierpinski.Basics]
x:586 [in Sierpinski.Basics]
x:588 [in Sierpinski.Basics]
x:590 [in Sierpinski.Basics]
x:592 [in Sierpinski.Basics]
x:594 [in Sierpinski.Basics]
x:595 [in Sierpinski.Basics]
x:596 [in Sierpinski.Basics]
X:597 [in Sierpinski.Basics]
x:6 [in Sierpinski.Hartogs]
x:601 [in Sierpinski.Basics]
X:603 [in Sierpinski.Basics]
X:607 [in Sierpinski.Basics]
x:61 [in Sierpinski.Basics]
X:611 [in Sierpinski.Basics]
X:615 [in Sierpinski.Basics]
X:619 [in Sierpinski.Basics]
X:621 [in Sierpinski.Basics]
X:627 [in Sierpinski.Basics]
x:63 [in Sierpinski.Basics]
x:635 [in Sierpinski.Basics]
X:637 [in Sierpinski.Basics]
X:647 [in Sierpinski.Basics]
x:66 [in Sierpinski.Sierpinski]
x:68 [in Sierpinski.Cardinality]
x:69 [in Sierpinski.Cardinality]
x:71 [in Sierpinski.Cardinality]
x:71 [in Sierpinski.Basics]
x:73 [in Sierpinski.Cardinality]
x:74 [in Sierpinski.Basics]
x:8 [in Sierpinski.Hartogs]
x:80 [in Sierpinski.Ordinals]
x:85 [in Sierpinski.Basics]
x:86 [in Sierpinski.Cardinality]
x:87 [in Sierpinski.Ordinals]
x:87 [in Sierpinski.Cardinality]
x:88 [in Sierpinski.Cardinality]
x:89 [in Sierpinski.Cardinality]
x:89 [in Sierpinski.Basics]
x:9 [in Sierpinski.Sierpinski]
x:92 [in Sierpinski.Basics]
x:96 [in Sierpinski.Basics]
Y
y':12 [in Sierpinski.Basics]y':377 [in Sierpinski.Basics]
y':381 [in Sierpinski.Basics]
y':395 [in Sierpinski.Basics]
y':401 [in Sierpinski.Basics]
y':411 [in Sierpinski.Basics]
y':412 [in Sierpinski.Basics]
y:11 [in Sierpinski.Sierpinski]
y:11 [in Sierpinski.Basics]
y:110 [in Sierpinski.Basics]
y:122 [in Sierpinski.Cardinality]
y:126 [in Sierpinski.Cardinality]
y:137 [in Sierpinski.Ordinals]
y:138 [in Sierpinski.Basics]
y:144 [in Sierpinski.Cardinality]
y:145 [in Sierpinski.Cardinality]
y:147 [in Sierpinski.Basics]
y:150 [in Sierpinski.Ordinals]
y:152 [in Sierpinski.Ordinals]
y:154 [in Sierpinski.Ordinals]
y:156 [in Sierpinski.Ordinals]
y:158 [in Sierpinski.Ordinals]
y:166 [in Sierpinski.Basics]
y:176 [in Sierpinski.Ordinals]
y:178 [in Sierpinski.Ordinals]
y:180 [in Sierpinski.Ordinals]
y:183 [in Sierpinski.Ordinals]
y:185 [in Sierpinski.Cardinality]
y:187 [in Sierpinski.Ordinals]
y:187 [in Sierpinski.Cardinality]
y:187 [in Sierpinski.Basics]
y:189 [in Sierpinski.Ordinals]
y:190 [in Sierpinski.Cardinality]
y:192 [in Sierpinski.Cardinality]
y:193 [in Sierpinski.Ordinals]
y:195 [in Sierpinski.Ordinals]
y:198 [in Sierpinski.Ordinals]
y:199 [in Sierpinski.Ordinals]
y:200 [in Sierpinski.Ordinals]
y:202 [in Sierpinski.Ordinals]
y:205 [in Sierpinski.Basics]
y:207 [in Sierpinski.Ordinals]
y:209 [in Sierpinski.Ordinals]
y:209 [in Sierpinski.Basics]
y:213 [in Sierpinski.Basics]
y:215 [in Sierpinski.Basics]
y:217 [in Sierpinski.Basics]
y:232 [in Sierpinski.Basics]
y:234 [in Sierpinski.Basics]
y:236 [in Sierpinski.Ordinals]
y:237 [in Sierpinski.Basics]
y:239 [in Sierpinski.Basics]
y:25 [in Sierpinski.Sierpinski]
y:256 [in Sierpinski.Basics]
y:260 [in Sierpinski.Basics]
y:264 [in Sierpinski.Basics]
y:266 [in Sierpinski.Basics]
y:268 [in Sierpinski.Basics]
y:27 [in Sierpinski.Sierpinski]
y:3 [in Sierpinski.Sierpinski]
y:308 [in Sierpinski.Basics]
y:311 [in Sierpinski.Basics]
y:324 [in Sierpinski.Basics]
y:34 [in Sierpinski.Basics]
y:373 [in Sierpinski.Basics]
y:376 [in Sierpinski.Basics]
y:380 [in Sierpinski.Basics]
y:385 [in Sierpinski.Basics]
y:389 [in Sierpinski.Basics]
y:394 [in Sierpinski.Basics]
y:400 [in Sierpinski.Basics]
y:406 [in Sierpinski.Basics]
y:41 [in Sierpinski.Basics]
y:410 [in Sierpinski.Basics]
y:416 [in Sierpinski.Basics]
y:421 [in Sierpinski.Basics]
y:46 [in Sierpinski.Ordinals]
y:5 [in Sierpinski.Cardinality]
y:50 [in Sierpinski.Ordinals]
y:53 [in Sierpinski.Ordinals]
Y:533 [in Sierpinski.Basics]
Y:538 [in Sierpinski.Basics]
y:54 [in Sierpinski.Ordinals]
y:540 [in Sierpinski.Basics]
y:55 [in Sierpinski.Ordinals]
Y:553 [in Sierpinski.Basics]
y:556 [in Sierpinski.Basics]
y:559 [in Sierpinski.Basics]
Y:561 [in Sierpinski.Basics]
Y:563 [in Sierpinski.Basics]
y:571 [in Sierpinski.Basics]
Y:573 [in Sierpinski.Basics]
Y:581 [in Sierpinski.Basics]
Y:598 [in Sierpinski.Basics]
y:602 [in Sierpinski.Basics]
Y:604 [in Sierpinski.Basics]
Y:608 [in Sierpinski.Basics]
Y:612 [in Sierpinski.Basics]
Y:616 [in Sierpinski.Basics]
Y:628 [in Sierpinski.Basics]
Y:638 [in Sierpinski.Basics]
Y:648 [in Sierpinski.Basics]
y:67 [in Sierpinski.Sierpinski]
y:7 [in Sierpinski.Hartogs]
y:70 [in Sierpinski.Cardinality]
y:72 [in Sierpinski.Cardinality]
y:81 [in Sierpinski.Ordinals]
y:84 [in Sierpinski.Basics]
y:88 [in Sierpinski.Ordinals]
y:9 [in Sierpinski.Hartogs]
y:90 [in Sierpinski.Basics]
y:95 [in Sierpinski.Basics]
Z
z:210 [in Sierpinski.Basics]z:218 [in Sierpinski.Basics]
z:232 [in Sierpinski.Ordinals]
z:235 [in Sierpinski.Basics]
z:240 [in Sierpinski.Basics]
z:277 [in Sierpinski.Basics]
z:292 [in Sierpinski.Basics]
z:298 [in Sierpinski.Basics]
z:312 [in Sierpinski.Basics]
z:404 [in Sierpinski.Basics]
z:415 [in Sierpinski.Basics]
z:426 [in Sierpinski.Basics]
other
α:138 [in Sierpinski.Ordinals]α:142 [in Sierpinski.Ordinals]
α:143 [in Sierpinski.Ordinals]
α:147 [in Sierpinski.Ordinals]
α:163 [in Sierpinski.Ordinals]
α:181 [in Sierpinski.Ordinals]
α:184 [in Sierpinski.Ordinals]
α:204 [in Sierpinski.Ordinals]
α:210 [in Sierpinski.Ordinals]
α:212 [in Sierpinski.Ordinals]
α:213 [in Sierpinski.Ordinals]
α:221 [in Sierpinski.Ordinals]
α:224 [in Sierpinski.Ordinals]
α:226 [in Sierpinski.Ordinals]
α:227 [in Sierpinski.Ordinals]
α:68 [in Sierpinski.Sierpinski]
α:69 [in Sierpinski.Sierpinski]
β:148 [in Sierpinski.Ordinals]
β:185 [in Sierpinski.Ordinals]
β:205 [in Sierpinski.Ordinals]
β:211 [in Sierpinski.Ordinals]
β:222 [in Sierpinski.Ordinals]
λ:225 [in Sierpinski.Ordinals]
ξ:159 [in Sierpinski.Ordinals]
ξ:160 [in Sierpinski.Ordinals]
ξ:161 [in Sierpinski.Ordinals]
ξ:162 [in Sierpinski.Ordinals]
ξ:191 [in Sierpinski.Ordinals]
Library Index
B
BasicsC
CardinalityH
HartogsO
OrdinalsS
SierpinskiLemma Index
A
AC_equiv' [in Sierpinski.Sierpinski]AC_equiv [in Sierpinski.Sierpinski]
B
bijection_to_injection [in Sierpinski.Cardinality]bijection_is_injective [in Sierpinski.Cardinality]
bijection_relation_transitivity [in Sierpinski.Cardinality]
bijection_relation_symmetry [in Sierpinski.Cardinality]
bijection_relation_reflexivity [in Sierpinski.Cardinality]
C
cancel_inverse_left [in Sierpinski.Cardinality]cancel_inverse_right [in Sierpinski.Cardinality]
cantors_theorem [in Sierpinski.Cardinality]
cartesian_product_upper_bound [in Sierpinski.Basics]
cartesian_product_eta [in Sierpinski.Basics]
class_as_set_equiv_set [in Sierpinski.Cardinality]
comprehension_condition [in Sierpinski.Basics]
D
decode_encode [in Sierpinski.Ordinals]description_is_solution [in Sierpinski.Basics]
disjoint_union_is_increasing_on_right [in Sierpinski.Cardinality]
disjoint_union_is_increasing_on_left [in Sierpinski.Cardinality]
disjoint_union_associative [in Sierpinski.Cardinality]
disjoint_union_iter_reduction_right [in Sierpinski.Basics]
disjoint_union_iter_reduction_left [in Sierpinski.Basics]
disjoint_union_iter_property [in Sierpinski.Basics]
E
element_equality [in Sierpinski.Basics]empty_set_ind [in Sierpinski.Basics]
encode_fun_el [in Sierpinski.Basics]
exists_element_of_explicit_set_iff [in Sierpinski.Basics]
explicit_set_equals_explicit_set_iff [in Sierpinski.Basics]
explicit_set_is_subset_of_explicit_set_iff [in Sierpinski.Basics]
extract_from_right_is_injective [in Sierpinski.Basics]
F
forall_elements_of_explicit_set_iff [in Sierpinski.Basics]from_left_or_right [in Sierpinski.Basics]
function_compose_inverse [in Sierpinski.Cardinality]
H
hartogs_number_has_upper_bound [in Sierpinski.Hartogs]hartogs_number_is_not_smaller [in Sierpinski.Hartogs]
hartogs_number_as_class_is_a_set [in Sierpinski.Hartogs]
hartogs_number_as_class_has_upper_bound [in Sierpinski.Hartogs]
I
image_of_injection_is_equipotent [in Sierpinski.Cardinality]image_under_id [in Sierpinski.Basics]
image_of_image [in Sierpinski.Basics]
injection_relation_transitivity [in Sierpinski.Cardinality]
injection_relation_reflexivity [in Sierpinski.Cardinality]
inj1_extract_from_left [in Sierpinski.Basics]
inj1_and_inj2_are_disjoint [in Sierpinski.Basics]
inj1_is_injective [in Sierpinski.Basics]
inj2_is_injective [in Sierpinski.Basics]
inverse_compose_function [in Sierpinski.Cardinality]
inverse_flip [in Sierpinski.Basics]
inverse_surjective [in Sierpinski.Basics]
inverse_injective [in Sierpinski.Basics]
in_class_as_set_iff [in Sierpinski.Cardinality]
in_Numeral_iff [in Sierpinski.Basics]
in_difference_iff [in Sierpinski.Basics]
in_intersection_iff [in Sierpinski.Basics]
in_indexed_intersection_iff [in Sierpinski.Basics]
in_indexed_union_iff [in Sierpinski.Basics]
in_explicit_set_iff [in Sierpinski.Basics]
in_adjunction_iff [in Sierpinski.Basics]
in_union_iff [in Sierpinski.Basics]
in_provisional_singleton [in Sierpinski.Basics]
in_provisional_unordered_pair_iff [in Sierpinski.Basics]
in_comprehension_iff_typed [in Sierpinski.Basics]
in_comprehension_iff [in Sierpinski.Basics]
in_conditional_fun_replacement_iff [in Sierpinski.Basics]
in_image_iff [in Sierpinski.Basics]
in_fun_replacement_iff [in Sierpinski.Basics]
isomorphic_ordinals_are_equal [in Sierpinski.Ordinals]
isomorphism_relation_symmetry [in Sierpinski.Ordinals]
isomorphism_relation_transitivity [in Sierpinski.Ordinals]
isomorphism_relation_reflexivity [in Sierpinski.Ordinals]
isomorphism_preserves_relation [in Sierpinski.Ordinals]
L
left_projection_beta [in Sierpinski.Basics]lemma1 [in Sierpinski.Sierpinski]
lemma2 [in Sierpinski.Sierpinski]
linearity [in Sierpinski.Ordinals]
N
nat_to_numeral_is_injective [in Sierpinski.Basics]nat_to_numeral_is_monotone [in Sierpinski.Basics]
nat_to_numeral_is_nat_to_numeral' [in Sierpinski.Basics]
not_gt_implies_leq [in Sierpinski.Ordinals]
no_set_equals_its_power_set [in Sierpinski.Basics]
no_set_contains_itself [in Sierpinski.Basics]
Numeral_equipotent_Numeral_plus_one [in Sierpinski.Cardinality]
Numeral_iter_reduction_S [in Sierpinski.Basics]
Numeral_iter_reduction_O [in Sierpinski.Basics]
Numeral_iter_property [in Sierpinski.Basics]
O
one_ind [in Sierpinski.Basics]ordinal_induction [in Sierpinski.Ordinals]
ordinal_is_element_iff_strict_sub [in Sierpinski.Ordinals]
ordinal_characterisation [in Sierpinski.Ordinals]
ordinal_is_transitive [in Sierpinski.Ordinals]
P
pair_is_injective_left [in Sierpinski.Basics]pair_is_injective_right [in Sierpinski.Basics]
power_set_equiv_power_set_plus_power_set [in Sierpinski.Cardinality]
power_set_of_disjoint_union [in Sierpinski.Cardinality]
power_set_is_increasing [in Sierpinski.Cardinality]
proof_irrelevance [in Sierpinski.Basics]
R
right_projection_beta [in Sierpinski.Basics]S
setlike_funspace_firstorder [in Sierpinski.Basics]setlike_funspace_firstorder' [in Sierpinski.Basics]
setlike_setlike' [in Sierpinski.Basics]
setlike_power [in Sierpinski.Basics]
setlike_funspace2 [in Sierpinski.Basics]
setlike_sum [in Sierpinski.Basics]
setlike_prod [in Sierpinski.Basics]
setlike_Prop [in Sierpinski.Basics]
setlike_props [in Sierpinski.Basics]
setlike_nat [in Sierpinski.Basics]
set_equipotent_set_plus_one [in Sierpinski.Cardinality]
set_equipotent_subset_plus_difference [in Sierpinski.Cardinality]
set_equals_subset_union_difference [in Sierpinski.Cardinality]
sierpinskis_theorem [in Sierpinski.Sierpinski]
small_class_is_a_set [in Sierpinski.Cardinality]
strict_well_order_is_strict_well_order' [in Sierpinski.Ordinals]
strict_well_order_has_least_elements [in Sierpinski.Ordinals]
strict_well_order_has_least_elements' [in Sierpinski.Ordinals]
strip_element [in Sierpinski.Basics]
subset_extensionality [in Sierpinski.Basics]
symmetric_cartesian_product_is_increasing [in Sierpinski.Cardinality]
T
transported_relation_is_isomorphic [in Sierpinski.Ordinals]two_is_power_set_of_one [in Sierpinski.Cardinality]
two_times_set_is_disjoin_union [in Sierpinski.Basics]
U
union_of_disjoints_equipotent_disjoint_union [in Sierpinski.Cardinality]unordered_pair_equals_unordered_pair_iff [in Sierpinski.Basics]
untyped_pair_is_injective_right [in Sierpinski.Basics]
untyped_pair_is_injective_left [in Sierpinski.Basics]
W
Well_Ordering_to_Choice [in Sierpinski.Sierpinski]Well_Ordering_to_Choice' [in Sierpinski.Sierpinski]
well_founded_induction [in Sierpinski.Basics]
Constructor Index
B
build_strict_well_order [in Sierpinski.Ordinals]build_surjection [in Sierpinski.Cardinality]
build_injection [in Sierpinski.Cardinality]
build_bijection [in Sierpinski.Cardinality]
build_is_unique_solution [in Sierpinski.Basics]
build_element [in Sierpinski.Basics]
build_class [in Sierpinski.Basics]
F
functionality [in Sierpinski.Basics]I
in_class [in Sierpinski.Basics]is_accessible_intro [in Sierpinski.Basics]
T
transitive_set_of_ordinals_is_ordinal [in Sierpinski.Ordinals]Axiom Index
B
big_union [in Sierpinski.Basics]E
empty_set [in Sierpinski.Basics]extensionality [in Sierpinski.Basics]
I
in_Numeral_iff' [in Sierpinski.Basics]in_replacement_iff [in Sierpinski.Basics]
in_power_set_iff [in Sierpinski.Basics]
in_big_union_iff [in Sierpinski.Basics]
in_empty_set_iff [in Sierpinski.Basics]
In_Set [in Sierpinski.Basics]
N
Numeral [in Sierpinski.Basics]P
PE [in Sierpinski.Basics]power_set [in Sierpinski.Basics]
R
replacement [in Sierpinski.Basics]S
sets_are_well_founded [in Sierpinski.Basics]Set_ [in Sierpinski.Basics]
Inductive Index
F
Functional [in Sierpinski.Basics]I
In_Class [in Sierpinski.Basics]Is_Ordinal [in Sierpinski.Ordinals]
Is_Accessible_By [in Sierpinski.Basics]
Projection Index
B
bijection_left_right [in Sierpinski.Cardinality]bijection_right_left [in Sierpinski.Cardinality]
bijection_to_left [in Sierpinski.Cardinality]
bijection_to_right [in Sierpinski.Cardinality]
E
element_property [in Sierpinski.Basics]element_value [in Sierpinski.Basics]
element_predicate [in Sierpinski.Basics]
F
functionality [in Sierpinski.Basics]I
injection_property [in Sierpinski.Cardinality]injection_fun [in Sierpinski.Cardinality]
in_class [in Sierpinski.Basics]
S
strict_well_order_is_terminating [in Sierpinski.Ordinals]strict_well_order_is_trichotomous [in Sierpinski.Ordinals]
strict_well_order_is_transitive [in Sierpinski.Ordinals]
strict_well_order_relation [in Sierpinski.Ordinals]
surjection_is_surjective [in Sierpinski.Cardinality]
surjection_fun [in Sierpinski.Cardinality]
U
unique_solution_is_unique [in Sierpinski.Basics]unique_solution_is_solution [in Sierpinski.Basics]
Instance Index
B
bijection_subrelation_flipped_injection [in Sierpinski.Cardinality]bijection_subrelation_injection [in Sierpinski.Cardinality]
D
description_is_unique [in Sierpinski.Basics]E
element_relation_on_O_is_well_founded [in Sierpinski.Ordinals]element_of_ordinal_is_ordinal [in Sierpinski.Ordinals]
element_of_tail_is_element_of_adjunction [in Sierpinski.Basics]
element_stays_element [in Sierpinski.Basics]
empty_set_is_ordinal [in Sierpinski.Ordinals]
F
fun_replacement_in_power_set [in Sierpinski.Basics]H
head_is_element_of_adjunction [in Sierpinski.Basics]I
in_indexed_union [in Sierpinski.Basics]in_union_intro_right [in Sierpinski.Basics]
in_union_intro_left [in Sierpinski.Basics]
in_union_intro2 [in Sierpinski.Basics]
in_union_intro1 [in Sierpinski.Basics]
in_image_of [in Sierpinski.Basics]
in_image_under [in Sierpinski.Basics]
in_set_if_in_subset [in Sierpinski.Basics]
in_class_of_all_sets [in Sierpinski.Basics]
O
ordinal_is_transitive' [in Sierpinski.Ordinals]R
reflexive_closure_is_partial_order [in Sierpinski.Ordinals]reflexive_closure_is_pre_order [in Sierpinski.Ordinals]
S
set_in_power_set [in Sierpinski.Basics]strict_well_order_on_ordinal [in Sierpinski.Ordinals]
strict_well_order_on_O [in Sierpinski.Ordinals]
strict_well_order_is_strict_order [in Sierpinski.Ordinals]
subset_subrelation_injection [in Sierpinski.Cardinality]
subset_relation_transitivity [in Sierpinski.Basics]
subset_relation_reflexivity [in Sierpinski.Basics]
successor_is_ordinal [in Sierpinski.Ordinals]
U
union_is_ordinal [in Sierpinski.Ordinals]Section Index
D
Description [in Sierpinski.Basics]Abbreviation Index
E
element [in Sierpinski.Basics]S
S [in Sierpinski.Basics]other
σ [in Sierpinski.Basics]Definition Index
A
adjunction [in Sierpinski.Basics]All [in Sierpinski.Basics]
Any [in Sierpinski.Basics]
Axiom_Of_Choice'' [in Sierpinski.Sierpinski]
Axiom_Of_Choice' [in Sierpinski.Sierpinski]
Axiom_Of_Choice [in Sierpinski.Sierpinski]
B
biject [in Sierpinski.Basics]bijection_relation_on_Set [in Sierpinski.Cardinality]
bijection_relation [in Sierpinski.Cardinality]
C
cartesian_product [in Sierpinski.Basics]class_as_set [in Sierpinski.Cardinality]
class_of_all_sets [in Sierpinski.Basics]
compose_isos [in Sierpinski.Ordinals]
compose_injections [in Sierpinski.Cardinality]
compose_bijections [in Sierpinski.Cardinality]
comprehension [in Sierpinski.Basics]
conditional_fun_replacement [in Sierpinski.Basics]
D
decode [in Sierpinski.Ordinals]description [in Sierpinski.Basics]
difference [in Sierpinski.Basics]
Disjoint [in Sierpinski.Cardinality]
disjoint_union_ind [in Sierpinski.Basics]
disjoint_union_iter [in Sierpinski.Basics]
Disjoint_Union_Iter_Property [in Sierpinski.Basics]
disjoint_union [in Sierpinski.Basics]
E
encode [in Sierpinski.Ordinals]encode_funspace_firstorder [in Sierpinski.Basics]
encode_funspace2 [in Sierpinski.Basics]
encode_fun [in Sierpinski.Basics]
encode_props [in Sierpinski.Basics]
encodings [in Sierpinski.Ordinals]
explicit_set [in Sierpinski.Basics]
extract_from_right [in Sierpinski.Basics]
extract_from_left [in Sierpinski.Basics]
F
foundation [in Sierpinski.Basics]fun_replacement [in Sierpinski.Basics]
G
Generalized_Continuum_Hypothesis [in Sierpinski.Sierpinski]Greater [in Sierpinski.Ordinals]
H
hartogs_number [in Sierpinski.Hartogs]hartogs_number_as_class [in Sierpinski.Hartogs]
Has_Least_Elements [in Sierpinski.Ordinals]
I
id_injection [in Sierpinski.Cardinality]id_bijection [in Sierpinski.Cardinality]
image_of [in Sierpinski.Basics]
image_under [in Sierpinski.Basics]
indexed_intersection [in Sierpinski.Basics]
indexed_union [in Sierpinski.Basics]
Infinite [in Sierpinski.Sierpinski]
injection_relation_on_Set [in Sierpinski.Cardinality]
injection_relation [in Sierpinski.Cardinality]
injection_as_bijection_into_image [in Sierpinski.Cardinality]
injective [in Sierpinski.Basics]
inj1 [in Sierpinski.Basics]
inj2 [in Sierpinski.Basics]
intersection [in Sierpinski.Basics]
inverse [in Sierpinski.Basics]
inverse_bijection [in Sierpinski.Cardinality]
Isomorphism [in Sierpinski.Ordinals]
isomorphism_relation [in Sierpinski.Ordinals]
isomorphism_inverse [in Sierpinski.Ordinals]
isomorphism_to_bijection [in Sierpinski.Ordinals]
Is_Limit [in Sierpinski.Ordinals]
Is_Strict_Well_Order' [in Sierpinski.Ordinals]
Is_Transitive_Set [in Sierpinski.Ordinals]
Is_Trichotomous [in Sierpinski.Ordinals]
Is_A_Set [in Sierpinski.Cardinality]
Is_From_Right [in Sierpinski.Basics]
Is_From_Left [in Sierpinski.Basics]
Is_Terminating [in Sierpinski.Basics]
Is_Subclass_Of [in Sierpinski.Basics]
L
least_element [in Sierpinski.Ordinals]left_projection [in Sierpinski.Basics]
Less [in Sierpinski.Ordinals]
Less_Or_Equal [in Sierpinski.Cardinality]
N
nat_to_numeral [in Sierpinski.Basics]nat_to_numeral' [in Sierpinski.Basics]
Numeral_iter [in Sierpinski.Basics]
Numeral_iter_Property [in Sierpinski.Basics]
Numeral_ind [in Sierpinski.Basics]
numeral_S [in Sierpinski.Basics]
numeral_O [in Sierpinski.Basics]
O
O [in Sierpinski.Ordinals]ordinal_upper_bound [in Sierpinski.Ordinals]
P
pair [in Sierpinski.Basics]Preserves_Relation [in Sierpinski.Ordinals]
provisional_singleton [in Sierpinski.Basics]
provisional_unordered_pair [in Sierpinski.Basics]
R
reflexive_closure [in Sierpinski.Ordinals]restrict_ordinal_isomorphism [in Sierpinski.Ordinals]
restrict_well_order [in Sierpinski.Ordinals]
right_projection [in Sierpinski.Basics]
S
setlike [in Sierpinski.Basics]setlike' [in Sierpinski.Basics]
set_to_class [in Sierpinski.Basics]
solutions [in Sierpinski.Basics]
strict_well_order_as_function [in Sierpinski.Ordinals]
successor_ordinal [in Sierpinski.Ordinals]
surjective [in Sierpinski.Basics]
T
transport_strict_well_order [in Sierpinski.Ordinals]transport_relation [in Sierpinski.Ordinals]
U
union [in Sierpinski.Basics]untyped_pair [in Sierpinski.Basics]
W
Well_Ordering_Theorem [in Sierpinski.Sierpinski]Z
zero_ordinal [in Sierpinski.Ordinals]Record Index
B
Bijection [in Sierpinski.Cardinality]C
Class [in Sierpinski.Basics]E
Element_Of [in Sierpinski.Basics]F
Functional [in Sierpinski.Basics]I
Injection [in Sierpinski.Cardinality]In_Class [in Sierpinski.Basics]
Is_Unique_Solution_Of [in Sierpinski.Basics]
S
Strict_Well_Order_On [in Sierpinski.Ordinals]Surjection [in Sierpinski.Cardinality]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1487 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1124 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (127 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (31 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (104 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |