Home | Metamath
Proof Explorer Theorem List (p. 133 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 | hashdif 13201 | The size of the difference of a finite set and another set is the first set's size minus that of the intersection of both. (Contributed by Steve Rodriguez, 24-Oct-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashdifsn 13202 | The size of the difference of a finite set and a singleton subset is the set's size minus 1. (Contributed by Alexander van der Vekens, 6-Jan-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashdifpr 13203 | The size of the difference of a finite set and a proper ordered pair subset is the set's size minus 2. (Contributed by AV, 16-Dec-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashsn01 13204 | The size of a singleton is either 0 or 1. (Contributed by AV, 23-Feb-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashsnle1 13205 | The size of a singleton is less than or equal to 1. (Contributed by AV, 23-Feb-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashsnlei 13206 | Get an upper bound on a concretely specified finite set. Base case: singleton set. (Contributed by Mario Carneiro, 11-Feb-2015.) (Proof shortened by AV, 23-Feb-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash1snb 13207* | The size of a set is 1 if and only if it is a singleton (containing a set). (Contributed by Alexander van der Vekens, 7-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | euhash1 13208* | The size of a set is 1 in terms of existential uniqueness. (Contributed by Alexander van der Vekens, 8-Feb-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash1n0 13209 | If the size of a set is 1 the set is not empty. (Contributed by AV, 23-Dec-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashgt12el 13210* | In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashgt12el2 13211* | In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashunlei 13212 | Get an upper bound on a concretely specified finite set. Induction step: union of two finite bounded sets. (Contributed by Mario Carneiro, 11-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashsslei 13213 | Get an upper bound on a concretely specified finite set. Transfer boundedness to a subset. (Contributed by Mario Carneiro, 11-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfz 13214 | Value of the numeric cardinality of a nonempty integer range. (Contributed by Stefan O'Rear, 12-Sep-2014.) (Proof shortened by Mario Carneiro, 15-Apr-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fzsdom2 13215 | Condition for finite ranges to have a strict dominance relation. (Contributed by Stefan O'Rear, 12-Sep-2014.) (Revised by Mario Carneiro, 15-Apr-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfzo 13216 | Cardinality of a half-open set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
..^ | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfzo0 13217 | Cardinality of a half-open set of integers based at zero. (Contributed by Stefan O'Rear, 15-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
..^ | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfzp1 13218 | Value of the numeric cardinality of a (possibly empty) integer range. (Contributed by AV, 19-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfz0 13219 | Value of the numeric cardinality of a nonempty range of nonnegative integers. (Contributed by Alexander van der Vekens, 21-Jul-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashxplem 13220 | Lemma for hashxp 13221. (Contributed by Paul Chapman, 30-Nov-2012.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashxp 13221 | The size of the Cartesian product of two finite sets is the product of their sizes. (Contributed by Paul Chapman, 30-Nov-2012.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashmap 13222 | The size of the set exponential of two finite sets is the exponential of their sizes. (This is the original motivation behind the notation for set exponentiation.) (Contributed by Mario Carneiro, 5-Aug-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashpw 13223 | The size of the power set of a finite set is 2 raised to the power of the size of the set. (Contributed by Paul Chapman, 30-Nov-2012.) (Proof shortened by Mario Carneiro, 5-Aug-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfun 13224 | A finite set is a function iff it is equinumerous to its domain. (Contributed by Mario Carneiro, 26-Sep-2013.) (Revised by Mario Carneiro, 12-Mar-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashres 13225 | The number of elements of a finite function restricted to a subset of its domain is equal to the number of elements of that subset. (Contributed by AV, 15-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashreshashfun 13226 | The number of elements of a finite function expressed by a restriction. (Contributed by AV, 15-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashimarn 13227 | The size of the image of a one-to-one function under the range of a function which is a one-to-one function into the domain of equals the size of the function . (Contributed by Alexander van der Vekens, 4-Feb-2018.) (Proof shortened by AV, 4-May-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
..^ | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashimarni 13228 | If the size of the image of a one-to-one function under the range of a function which is a one-to-one function into the domain of is a nonnegative integer, the size of the function is the same nonnegative integer. (Contributed by Alexander van der Vekens, 4-Feb-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
..^ | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | resunimafz0 13229 | TODO-AV: Revise using Word ? Formerly part of proof of eupth2lem3 27096: The union of a restriction by an image over an open range of nonnegative integers and a singleton of an ordered pair is a restriction by an image over an interval of nonnegative integers. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 20-Feb-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
..^ ..^ ..^ | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fnfz0hash 13230 | The size of a function on a finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 25-Jun-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ffz0hash 13231 | The size of a function on a finite set of sequential nonnegative integers equals the upper bound of the sequence increased by 1. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Proof shortened by AV, 11-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fnfz0hashnn0 13232 | The size of a function on a finite set of sequential nonnegative integers is a nonnegative integer. (Contributed by AV, 10-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ffzo0hash 13233 | The size of a function on a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 25-Mar-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
..^ | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fnfzo0hash 13234 | The size of a function on a half-open range of nonnegative integers equals the upper bound of this range. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Proof shortened by AV, 11-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
..^ | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fnfzo0hashnn0 13235 | The value of the size function on a half-open range of nonnegative integers is a nonnegative integer. (Contributed by AV, 10-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
..^ | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashbclem 13236* | Lemma for hashbc 13237: inductive step. (Contributed by Mario Carneiro, 13-Jul-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashbc 13237* | The binomial coefficient counts the number of subsets of a finite set of a given size. This is Metamath 100 proof #58 (formula for the number of combinations). (Contributed by Mario Carneiro, 13-Jul-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfacen 13238* | The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashf1lem1 13239* | Lemma for hashf1 13241. (Contributed by Mario Carneiro, 17-Apr-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashf1lem2 13240* | Lemma for hashf1 13241. (Contributed by Mario Carneiro, 17-Apr-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashf1 13241* | The permutation number counts the number of injections from to . (Contributed by Mario Carneiro, 21-Jan-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfac 13242* | A factorial counts the number of bijections on a finite set. (Contributed by Mario Carneiro, 21-Jan-2015.) (Proof shortened by Mario Carneiro, 17-Apr-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | leiso 13243 | Two ways to write a strictly increasing function on the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | leisorel 13244 | Version of isorel 6576 for strictly increasing functions on the reals. (Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro, 9-Sep-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fz1isolem 13245* | Lemma for fz1iso 13246. (Contributed by Mario Carneiro, 2-Apr-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
OrdIso | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fz1iso 13246* | Any finite ordered set has an order isometry to a one-based finite sequence. (Contributed by Mario Carneiro, 2-Apr-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ishashinf 13247* | Any set that is not finite contains subsets of arbitrarily large finite cardinality. Cf. isinf 8173. (Contributed by Thierry Arnoux, 5-Jul-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | seqcoll 13248* | The function contains a sparse set of nonzero values to be summed. The function is an order isomorphism from the set of nonzero values of to a 1-based finite sequence, and collects these nonzero values together. Under these conditions, the sum over the values in yields the same result as the sum over the original set . (Contributed by Mario Carneiro, 2-Apr-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | seqcoll2 13249* | The function contains a sparse set of nonzero values to be summed. The function is an order isomorphism from the set of nonzero values of to a 1-based finite sequence, and collects these nonzero values together. Under these conditions, the sum over the values in yields the same result as the sum over the original set . (Contributed by Mario Carneiro, 13-Dec-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashprlei 13250 | An unordered pair has at most two elements. (Contributed by Mario Carneiro, 11-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2pr 13251* | A set of size two is an unordered pair. (Contributed by Alexander van der Vekens, 8-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2prde 13252* | A set of size two is an unordered pair of two different elements. (Contributed by Alexander van der Vekens, 8-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2exprb 13253* | A set of size two is an unordered pair if and only if it contains two different elements. (Contributed by Alexander van der Vekens, 14-Jan-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2prb 13254* | A set of size two is a proper unordered pair. (Contributed by AV, 1-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | prprrab 13255 | The set of proper pairs of elements of a given set expressed in two ways. (Contributed by AV, 24-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nehash2 13256 | The cardinality of a set with two distinct elements. (Contributed by Thierry Arnoux, 27-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2prd 13257 | A set of size two is an unordered pair if it contains two different elements. (Contributed by Alexander van der Vekens, 9-Dec-2018.) (Proof shortened by AV, 1-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2pwpr 13258 | If the size of a subset of an unordered pair is 2, the subset is the pair itself. (Contributed by Alexander van der Vekens, 9-Dec-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashle2pr 13259* | A nonempty set of size less than or equal to two is an unordered pair of sets. (Contributed by AV, 24-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashle2prv 13260* | A nonempty subset of a powerset of a class has size less than or equal to two iff it is an unordered pair of elements of . (Contributed by AV, 24-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pr2pwpr 13261* | The set of subsets of a pair having length 2 is the set of the pair as singleton. (Contributed by AV, 9-Dec-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashge2el2dif 13262* | A set with size at least 2 has at least 2 different elements. (Contributed by AV, 18-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashge2el2difr 13263* | A set with at least 2 different elements has size at least 2. (Contributed by AV, 14-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashge2el2difb 13264* | A set has size at least 2 iff it has at least 2 different elements. (Contributed by AV, 14-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashdmpropge2 13265 | The size of the domain of a class which contains two ordered pairs with different first componens is greater than or mequal to 2. (Contributed by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashtplei 13266 | An unordered triple has at most three elements. (Contributed by Mario Carneiro, 11-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashtpg 13267 | The size of an unordered triple of three different elements. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 18-Sep-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashge3el3dif 13268* | A set with size at least 3 has at least 3 different elements. In contrast to hashge2el2dif 13262, which has an elementary proof, the dominance relation and 1-1 functions from a set with three elements which are known to be different are used to prove this theorem. Although there is also an elementary proof for this theorem, it might be much longer. After all, this proof should be kept because it can be used as template for proofs for higher cardinalities. (Contributed by AV, 20-Mar-2019.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | elss2prb 13269* | An element of the set of subsets with two elements is a proper unordered pair. (Contributed by AV, 1-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2sspr 13270* | A subset of size two is an unordered pair of elements of its superset. (Contributed by Alexander van der Vekens, 12-Jul-2017.) (Proof shortened by AV, 4-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | exprelprel 13271* | If there is an element of the set of subsets with two elements in a set, an unordered pair of sets is in the set. (Contributed by Alexander van der Vekens, 12-Jul-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash3tr 13272* | A set of size three is an unordered triple. (Contributed by Alexander van der Vekens, 13-Sep-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash1to3 13273* | If the size of a set is between 1 and 3 (inclusively), the set is a singleton or an unordered pair or an unordered triple. (Contributed by Alexander van der Vekens, 13-Sep-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fundmge2nop0 13274 | A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fundmge2nop 13275 (with the less restrictive requirement that needs to be a function instead of ) is useful for proofs for extensible structures, see structn0fun 15869. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 7-Jun-2021.) (Proof shortened by AV, 15-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fundmge2nop 13275 | A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 12-Oct-2020.) (Proof shortened by AV, 9-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fun2dmnop0 13276 | A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fun2dmnop 13277 (with the less restrictive requirement that needs to be a function instead of ) is useful for proofs for extensible structures, see structn0fun 15869. (Contributed by AV, 21-Sep-2020.) (Revised by AV, 7-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fun2dmnop 13277 | A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 9-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1indlem 13278 | TODO-AV1: no lemma, but self-reliant theorem! Lemma for brfi1ind 13281: The size of a set is the size of this set with one element removed, increased by 1. (Contributed by Alexander van der Vekens, 7-Jan-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fi1uzind 13279* | Properties of an ordered pair with a finite first component with at least L elements, proven by finite induction on the size of the first component. This theorem can be applied for graphs (represented as orderd pairs of vertices and edges) with a finite number of vertices, usually with (see opfi1ind 13284) or . (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1uzind 13280* | Properties of a binary relation with a finite first component with at least L elements, proven by finite induction on the size of the first component. This theorem can be applied for graphs (as binary relation between the set of vertices and an edge function) with a finite number of vertices, usually with (see brfi1ind 13281) or . (Contributed by Alexander van der Vekens, 7-Jan-2018.) (Proof shortened by AV, 23-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1ind 13281* | Properties of a binary relation with a finite first component, proven by finite induction on the size of the first component. (Contributed by Alexander van der Vekens, 7-Jan-2018.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1indALT 13282* | Alternate proof of brfi1ind 13281, which does not use brfi1uzind 13280. (Contributed by Alexander van der Vekens, 7-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opfi1uzind 13283* | Properties of an ordered pair with a finite first component with at least L elements, proven by finite induction on the size of the first component. This theorem can be applied for graphs (represented as orderd pairs of vertices and edges) with a finite number of vertices, usually with (see opfi1ind 13284) or . (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opfi1ind 13284* | Properties of an ordered pair with a finite first component, proven by finite induction on the size of the first component. This theorem can be applied for graphs (represented as orderd pairs of vertices and edges) with a finite number of vertices, e.g. fusgrfis 26222. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fi1uzindOLD 13285* | Obsolete version of fi1uzind 13279 as of 28-Mar-2021. (Contributed by AV, 22-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1uzindOLD 13286* | Obsolete version of brfi1uzind 13280 as of 28-Mar-2021. (Contributed by AV, 7-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1indOLD 13287* | Obsolete version of brfi1ind 13281 as of 28-Mar-2021. (Contributed by AV, 7-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1indALTOLD 13288* | Obsolete version of brfi1indALT 13282 as of 28-Mar-2021. (Contributed by AV, 7-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opfi1uzindOLD 13289* | Obsolete version of opfi1uzind 13283 as of 28-Mar-2021. (Contributed by AV, 22-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opfi1indOLD 13290* | Obsolete version of opfi1ind 13284 as of 28-Mar-2021. (Contributed by AV, 22-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
This section is about words (or strings) over a set (alphabet) defined as finite sequences of symbols (or characters) being elements of the alphabet. Although it is often required that the underlying set/alphabet be nonempty, finite and not a proper class, these restrictions are not made in the current definition df-word 13299, see, for example, s1cli 13384: Word . Note that the empty word (i.e. the empty set) is the only word over an empty alphabet, see 0wrd0 13331. The set Word of words over is the free monoid over , where the monoid law is concatenation and the monoid unit is the empty word. Besides the definition of words themselves, several operations on words are defined in this section:
| ||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cword 13291 | Syntax for the Word operator. | ||||||||||||||||||||||||||||||||||||||||||||||||||
Word | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | clsw 13292 | Extend class notation with the Last Symbol of a word. | ||||||||||||||||||||||||||||||||||||||||||||||||||
lastS | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cconcat 13293 | Syntax for the concatenation operator. | ||||||||||||||||||||||||||||||||||||||||||||||||||
++ | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cs1 13294 | Syntax for the singleton word constructor. | ||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | csubstr 13295 | Syntax for the subword operator. | ||||||||||||||||||||||||||||||||||||||||||||||||||
substr | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | csplice 13296 | Syntax for the word splicing operator. | ||||||||||||||||||||||||||||||||||||||||||||||||||
splice | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | creverse 13297 | Syntax for the word reverse operator. | ||||||||||||||||||||||||||||||||||||||||||||||||||
reverse | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | creps 13298 | Extend class notation with words consisting of one repeated symbol. | ||||||||||||||||||||||||||||||||||||||||||||||||||
repeatS | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-word 13299* | Define the class of words over a set. A word (sometimes also called a string) is a finite sequence of symbols from a set (alphabet) . Definition in section 9.1 of [AhoHopUll] p. 318. The domain is forced to be an initial segment of so that two words with the same symbols in the same order be equal. The set Word is sometimes denoted by S*, using the Kleene star, although the Kleene star, or Kleene closure, is sometimes reserved to denote an operation on languages. The set Word is the free monoid over , where the monoid law is concatenation and the monoid unit is the empty word (see frmdval 17388). (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 14-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
Word ..^ | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-lsw 13300 | Extract the last symbol of a word. May be not meaningful for other sets which are not words. The name lastS (as abbreviation of "lastSymbol") is a compromise between usually used names for corresponding functions in computer programs (as last() or lastChar()), the terminology used for words in set.mm ("symbol" instead of "character") and brevity ("lastS" is shorter than "lastChar" and "lastSymbol"). Labels of theorems about last symbols of a word will contain the abbreviation "lsw" (Last Symbol of a Word). (Contributed by Alexander van der Vekens, 18-Mar-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
lastS |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |