HomeTheorem List (p. 312 of 426)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 312 of 426) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | bnj1388 31101* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
       
 ![/\](wedge.gif "/\"){kind=small}       
        
        
          ![].](_drbrack.gif "]."){kind=small}  
| ||
| Theorem | bnj1398 31102* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
     
| ||
| Theorem | bnj1413 31103* |
Property of .
(Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(New usage is discouraged.)
|
 | ||
| Theorem | bnj1408 31104* | Technical lemma for bnj1414 31105. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ||
| Theorem | bnj1414 31105* |
Property of .
(Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(New usage is discouraged.)
|
|
| ||
| Theorem | bnj1415 31106* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1416 31107 | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ||
| Theorem | bnj1418 31108 |
Property of .
(Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(New usage is discouraged.)
|
|
| ||
| Theorem | bnj1417 31109* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.) |
| ||
| Theorem | bnj1421 31110* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ||
| Theorem | bnj1444 31111* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
 
| ||
| Theorem | bnj1445 31112* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
| ||
| Theorem | bnj1446 31113* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1447 31114* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1448 31115* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1449 31116* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1442 31117* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1450 31118* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1423 31119* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1452 31120* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1466 31121* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
 | ||
| Theorem | bnj1467 31122* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1463 31123* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1489 31124* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1491 31125* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1312 31126* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1493 31127* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1497 31128* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
 | ||
| Theorem | bnj1498 31129* | Technical lemma for bnj60 31130. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
 | ||
| Theorem | bnj60 31130* | Well-founded recursion, part 1 of 3. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1514 31131* | Technical lemma for bnj1500 31136. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1518 31132* | Technical lemma for bnj1500 31136. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1519 31133* | Technical lemma for bnj1500 31136. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1520 31134* | Technical lemma for bnj1500 31136. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1501 31135* | Technical lemma for bnj1500 31136. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1500 31136* | Well-founded recursion, part 2 of 3. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1525 31137* | Technical lemma for bnj1522 31140. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1529 31138* | Technical lemma for bnj1522 31140. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1523 31139* | Technical lemma for bnj1522 31140. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | bnj1522 31140* | Well-founded recursion, part 3 of 3. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
|
| ||
| Axiom | ax-7d 31141* | Distinct variable version of ax-11 2034. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| | ||
| Axiom | ax-8d 31142* | Distinct variable version of ax-7 1935. (Contributed by Mario Carneiro, 14-Aug-2015.) |
|
| ||
| Axiom | ax-9d1 31143 | Distinct variable version of ax-6 1888, equal variables case. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| | ||
| Axiom | ax-9d2 31144* | Distinct variable version of ax-6 1888, distinct variables case. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| | ||
| Axiom | ax-10d 31145* | Distinct variable version of axc11n 2307. (Contributed by Mario Carneiro, 14-Aug-2015.) |
|
| ||
| Axiom | ax-11d 31146* | Distinct variable version of ax-12 2047. (Contributed by Mario Carneiro, 14-Aug-2015.) |
|
| ||
| Theorem | quartfull 31147 | The quartic equation, written out in full. This actually makes a fairly good Metamath stress test. Note that the length of this formula could be shortened significantly if the intermediate expressions were expanded and simplified, but it's not like this theorem will be used anyway. (Contributed by Mario Carneiro, 6-May-2015.) |
        ;
;
 ;  ;;  ;
;
; ;; ; ; ;;   ;
;
; ;; ;
;
; ;; ; ; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;;
;
;
; ;; ;
;
; ;; ; ; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;;  ;
;
; ;; ;
;
; ;; ; ; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;;
;
;
; ;; ;
;
; ;; ; ; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; ; ; ;; ;
;
; ;; ;
;
; ;; ; ; ;; | ||
| Theorem | deranglem 31148* | Lemma for derangements. (Contributed by Mario Carneiro, 19-Jan-2015.) |
   | ||
| Theorem | derangval 31149* | Define the derangement function, which counts the number of bijections from a set to itself such that no element is mapped to itself. (Contributed by Mario Carneiro, 19-Jan-2015.) |
 
| ||
| Theorem | derangf 31150* | The derangement number is a function from finite sets to nonnegative integers. (Contributed by Mario Carneiro, 19-Jan-2015.) |
  | ||
| Theorem | derang0 31151* | The derangement number of the empty set. (Contributed by Mario Carneiro, 19-Jan-2015.) |
|
| ||
| Theorem | derangsn 31152* | The derangement number of a singleton. (Contributed by Mario Carneiro, 19-Jan-2015.) |
 | ||
| Theorem | derangenlem 31153* | One half of derangen 31154. (Contributed by Mario Carneiro, 22-Jan-2015.) |
  | ||
| Theorem | derangen 31154* | The derangement number is a cardinal invariant, i.e. it only depends on the size of a set and not on its contents. (Contributed by Mario Carneiro, 22-Jan-2015.) |
|
| ||
| Theorem | subfacval 31155* |
The subfactorial is defined as the number of derangements (see
derangval 31149) of the set   . (Contributed by Mario
Carneiro, 21-Jan-2015.)
|
  | ||
| Theorem | derangen2 31156* | Write the derangement number in terms of the subfactorial. (Contributed by Mario Carneiro, 22-Jan-2015.) |
|
| ||
| Theorem | subfacf 31157* | The subfactorial is a function from nonnegative integers to nonnegative integers. (Contributed by Mario Carneiro, 19-Jan-2015.) |
|
| ||
| Theorem | subfaclefac 31158* | The subfactorial is less than the factorial. (Contributed by Mario Carneiro, 19-Jan-2015.) |
 | ||
| Theorem | subfac0 31159* | The subfactorial at zero. (Contributed by Mario Carneiro, 19-Jan-2015.) |
|
| ||
| Theorem | subfac1 31160* | The subfactorial at one. (Contributed by Mario Carneiro, 19-Jan-2015.) |
|
| ||
| Theorem | subfacp1lem1 31161* |
Lemma for subfacp1 31168. The set  together with 
partitions the set . (Contributed by Mario
Carneiro, 23-Jan-2015.)
|
![\](setminus.gif "\"){kind=small}
| ||
| Theorem | subfacp1lem2a 31162* |
Lemma for subfacp1 31168. Properties of a bijection on
augmented with the two-element flip to get a bijection on
. (Contributed by Mario Carneiro,
23-Jan-2015.)
|
|
| ||
| Theorem | subfacp1lem2b 31163* |
Lemma for subfacp1 31168. Properties of a bijection on
augmented with the two-element flip to get a bijection on
. (Contributed by Mario Carneiro,
23-Jan-2015.)
|
|
| ||
| Theorem | subfacp1lem3 31164* |
Lemma for subfacp1 31168. In subfacp1lem6 31167 we cut up the set of all
derangements on first according to the value
at , and
then by whether or not
. In this lemma, we show that the
subset of all derangements that satisfy
this for fixed
is in bijection with derangements,
by
simply dropping the and
points from the
function to get a derangement on
.
(Contributed by Mario
Carneiro, 23-Jan-2015.)
|
|
| ||
| Theorem | subfacp1lem4 31165* |
Lemma for subfacp1 31168. The function , which swaps
with and
leaves all other elements alone, is a bijection of
order , i.e.
it is its own inverse. (Contributed by Mario
Carneiro, 19-Jan-2015.)
|
  | ||
| Theorem | subfacp1lem5 31166* |
Lemma for subfacp1 31168. In subfacp1lem6 31167 we cut up the set of all
derangements on first according to the value
at , and
then by whether or not
. In this lemma, we show that the
subset of all derangements with
for fixed is in
bijection with derangements of , because
pre-composing with the function swaps and and
turns the function into a bijection with and
for all other , so dropping the point
at yields a
derangement on the
remaining points.
(Contributed by Mario Carneiro, 23-Jan-2015.)
|
|
| ||
| Theorem | subfacp1lem6 31167* |
Lemma for subfacp1 31168. By induction, we cut up the set of all
derangements on according to the possible values of
(since
), and for each set for
fixed , the subset of derangements with
has size (by subfacp1lem3 31164),
while the subset with has size (by
subfacp1lem5 31166). Adding it all up yields the desired
equation
for the number of
derangements on
. (Contributed by Mario Carneiro, 22-Jan-2015.)
|
|
| ||
| Theorem | subfacp1 31168* | A two-term recurrence for the subfactorial. This theorem allows us to forget the combinatorial definition of the derangement number in favor of the recursive definition provided by this theorem and subfac0 31159, subfac1 31160. (Contributed by Mario Carneiro, 23-Jan-2015.) |
|
| ||
| Theorem | subfacval2 31169* | A closed-form expression for the subfactorial. (Contributed by Mario Carneiro, 23-Jan-2015.) |
 
| ||
| Theorem | subfaclim 31170* |
The subfactorial converges rapidly to
 . This is part of
Metamath 100 proof #88. (Contributed by Mario Carneiro,
23-Jan-2015.)
|
 | ||
| Theorem | subfacval3 31171* |
Another closed form expression for the subfactorial. The expression
 is a way
of saying "rounded to the nearest
integer". (Contributed by Mario Carneiro, 23-Jan-2015.)
|
|
| ||
| Theorem | derangfmla 31172* |
The derangements formula, which expresses the number of derangements of
a finite nonempty set in terms of the factorial. The expression
is a way
of saying "rounded to the nearest
integer". This is part of Metamath 100 proof #88. (Contributed by
Mario Carneiro, 23-Jan-2015.)
|
|
| ||
| Theorem | erdszelem1 31173* | Lemma for erdsze 31184. (Contributed by Mario Carneiro, 22-Jan-2015.) |
 
| ||
| Theorem | erdszelem2 31174* | Lemma for erdsze 31184. (Contributed by Mario Carneiro, 22-Jan-2015.) |
|
| ||
| Theorem | erdszelem3 31175* | Lemma for erdsze 31184. (Contributed by Mario Carneiro, 22-Jan-2015.) |
   | ||
| Theorem | erdszelem4 31176* | Lemma for erdsze 31184. (Contributed by Mario Carneiro, 22-Jan-2015.) |
 | ||
| Theorem | erdszelem5 31177* | Lemma for erdsze 31184. (Contributed by Mario Carneiro, 22-Jan-2015.) |
|
| ||
| Theorem | erdszelem6 31178* | Lemma for erdsze 31184. (Contributed by Mario Carneiro, 22-Jan-2015.) |
| | ||
| Theorem | erdszelem7 31179* | Lemma for erdsze 31184. (Contributed by Mario Carneiro, 22-Jan-2015.) |
| ||
| Theorem | erdszelem8 31180* | Lemma for erdsze 31184. (Contributed by Mario Carneiro, 22-Jan-2015.) |
|
| ||
| Theorem | erdszelem9 31181* | Lemma for erdsze 31184. (Contributed by Mario Carneiro, 22-Jan-2015.) |
    | ||
| Theorem | erdszelem10 31182* | Lemma for erdsze 31184. (Contributed by Mario Carneiro, 22-Jan-2015.) |
| ||
| Theorem | erdszelem11 31183* | Lemma for erdsze 31184. (Contributed by Mario Carneiro, 22-Jan-2015.) |
|
| ||
| Theorem | erdsze 31184* |
The Erdős-Szekeres theorem. For any injective sequence on
the reals of length at least , there is
either a subsequence of length at least on which is
increasing (i.e. a order isomorphism) or
a subsequence of
length at least on which
is decreasing (i.e. a
order isomorphism, recalling that is the greater-than
relation). This is part of Metamath 100 proof #73. (Contributed by
Mario Carneiro, 22-Jan-2015.)
|
|
| ||
| Theorem | erdsze2lem1 31185* | Lemma for erdsze2 31187. (Contributed by Mario Carneiro, 22-Jan-2015.) |
 | ||
| Theorem | erdsze2lem2 31186* | Lemma for erdsze2 31187. (Contributed by Mario Carneiro, 22-Jan-2015.) |
|
| ||
| Theorem | erdsze2 31187* |
Generalize the statement of the Erdős-Szekeres theorem erdsze 31184 to
"sequences" indexed by an arbitrary subset of , which can be
infinite. This is part of Metamath 100 proof #73. (Contributed by
Mario Carneiro, 22-Jan-2015.)
|
|
| ||
| Theorem | kur14lem1 31188 | Lemma for kur14 31198. (Contributed by Mario Carneiro, 17-Feb-2015.) |
|
| ||
| Theorem | kur14lem2 31189 |
Lemma for kur14 31198. Write interior in terms of closure and
complement:
  where is complement and is closure.
(Contributed by Mario Carneiro, 11-Feb-2015.)
|
   | ||
| Theorem | kur14lem3 31190 | Lemma for kur14 31198. A closure is a subset of the base set. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| | ||
| Theorem | kur14lem4 31191 | Lemma for kur14 31198. Complementation is an involution on the set of subsets of a topology. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| | ||
| Theorem | kur14lem5 31192 | Lemma for kur14 31198. Closure is an idempotent operation in the set of subsets of a topology. (Contributed by Mario Carneiro, 11-Feb-2015.) |
| | ||
| Theorem | kur14lem6 31193 |
Lemma for kur14 31198. If is the complementation operator and
is the closure operator, this expresses the identity
for any subset of the topological
space. This is the key result that lets us cut down long enough
sequences of that
arise when applying closure and
complement repeatedly to , and explains why we end up with a
number as large as , yet no
larger. (Contributed by Mario
Carneiro, 11-Feb-2015.)
|
| | ||
| Theorem | kur14lem7 31194 |
Lemma for kur14 31198: main proof. The set here contains all the
distinct combinations of and that can
arise, and we prove
here that applying or to any
element of yields
another
elemnt of . In
operator shorthand, we have
. From the identities
and
, we can reduce any operator combination
containing two
adjacent identical operators, which is why the list only contains
alternating sequences. The reason the sequences don't keep going after
a certain point is due to the identity ,
proved in kur14lem6 31193. (Contributed by Mario Carneiro,
11-Feb-2015.)
|
|
| ||
| Theorem | kur14lem8 31195 |
Lemma for kur14 31198. Show that the set contains at most
elements. (It could be less if some of the operators take the same
value for a given set, but Kuratowski showed that this upper bound of
is tight in the sense that there exist
topological spaces and
subsets of these spaces for which all
generated sets are
distinct, and indeed the real numbers form such a topological space.)
(Contributed by Mario Carneiro, 11-Feb-2015.)
|
|
; | ||
| Theorem | kur14lem9 31196* |
Lemma for kur14 31198. Since the set is closed under closure and
complement, it contains the minimal set as a subset, so also
has at most elements. (Indeed , and it's not hard to
prove this, but we don't need it for this proof.) (Contributed by Mario
Carneiro, 11-Feb-2015.)
|
 ; | ||
| Theorem | kur14lem10 31197* |
Lemma for kur14 31198. Discharge the set . (Contributed by Mario
Carneiro, 11-Feb-2015.)
|
|
; | ||
| Theorem | kur14 31198* | Kuratowski's closure-complement theorem. There are at most 14 sets which can be obtained by the application of the closure and complement operations to a set in a topological space. (Contributed by Mario Carneiro, 11-Feb-2015.) |
|
; | ||
| Syntax | cretr 31199 | Extend class notation with the retract relation. |
 Retr | ||
| Definition | df-retr 31200* |
Define the set of retractions on two topological spaces. We say that
is a
retraction from to
. or Retr iff
there is an
such that
are continuous
functions called the retraction and section respectively, and their
composite  is homotopic to the identity map. If a
retraction
exists, we say
is a retract of .
(This terminology is
borrowed from HoTT and appears to be nonstandard, although it has
similaries to the concept of retract in the category of topological
spaces and to a deformation retract in general topology.) Two
topological spaces that are retracts of each other are called homotopy
equivalent. (Contributed by Mario Carneiro, 11-Feb-2015.)
|
Retr 
  Htpy
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |