![]() |
Metamath
Proof Explorer Theorem List (p. 145 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashsnlei 14401 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ({π΄} β Fin β§ (β―β{π΄}) β€ 1) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash1snb 14402* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π β ((β―βπ) = 1 β βπ π = {π})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | euhash1 14403* | The size of a set is 1 in terms of existential uniqueness. (Contributed by Alexander van der Vekens, 8-Feb-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π β ((β―βπ) = 1 β β!π π β π)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash1n0 14404 | If the size of a set is 1 the set is not empty. (Contributed by AV, 23-Dec-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β π β§ (β―βπ΄) = 1) β π΄ β β ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashgt12el 14405* | In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β π β§ 1 < (β―βπ)) β βπ β π βπ β π π β π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashgt12el2 14406* | In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β π β§ 1 < (β―βπ) β§ π΄ β π) β βπ β π π΄ β π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashgt23el 14407* | A set with more than two elements has at least three different elements. (Contributed by BTernaryTau, 21-Sep-2023.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β π β§ 2 < (β―βπ)) β βπ β π βπ β π βπ β π (π β π β§ π β π β§ π β π)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashunlei 14408 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΆ = (π΄ βͺ π΅) & β’ (π΄ β Fin β§ (β―βπ΄) β€ πΎ) & β’ (π΅ β Fin β§ (β―βπ΅) β€ π) & β’ πΎ β β0 & β’ π β β0 & β’ (πΎ + π) = π β β’ (πΆ β Fin β§ (β―βπΆ) β€ π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashsslei 14409 | Get an upper bound on a concretely specified finite set. Transfer boundedness to a subset. (Contributed by Mario Carneiro, 11-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΅ β π΄ & β’ (π΄ β Fin β§ (β―βπ΄) β€ π) & β’ π β β0 β β’ (π΅ β Fin β§ (β―βπ΅) β€ π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfz 14410 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π΅ β (β€β₯βπ΄) β (β―β(π΄...π΅)) = ((π΅ β π΄) + 1)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fzsdom2 14411 | 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 14412 | Cardinality of a half-open set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π΅ β (β€β₯βπ΄) β (β―β(π΄..^π΅)) = (π΅ β π΄)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfzo0 14413 | Cardinality of a half-open set of integers based at zero. (Contributed by Stefan O'Rear, 15-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π΅ β β0 β (β―β(0..^π΅)) = π΅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfzp1 14414 | Value of the numeric cardinality of a (possibly empty) integer range. (Contributed by AV, 19-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π΅ β (β€β₯βπ΄) β (β―β((π΄ + 1)...π΅)) = (π΅ β π΄)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfz0 14415 | Value of the numeric cardinality of a nonempty range of nonnegative integers. (Contributed by Alexander van der Vekens, 21-Jul-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π΅ β β0 β (β―β(0...π΅)) = (π΅ + 1)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashxplem 14416 | Lemma for hashxp 14417. (Contributed by Paul Chapman, 30-Nov-2012.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΅ β Fin β β’ (π΄ β Fin β (β―β(π΄ Γ π΅)) = ((β―βπ΄) Β· (β―βπ΅))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashxp 14417 | The size of the Cartesian product of two finite sets is the product of their sizes. (Contributed by Paul Chapman, 30-Nov-2012.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β Fin β§ π΅ β Fin) β (β―β(π΄ Γ π΅)) = ((β―βπ΄) Β· (β―βπ΅))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashmap 14418 | 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.) (Proof shortened by AV, 18-Jul-2022.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β Fin β§ π΅ β Fin) β (β―β(π΄ βm π΅)) = ((β―βπ΄)β(β―βπ΅))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashpw 14419 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π΄ β Fin β (β―βπ« π΄) = (2β(β―βπ΄))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfun 14420 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (πΉ β Fin β (Fun πΉ β (β―βπΉ) = (β―βdom πΉ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashres 14421 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((Fun π΄ β§ π΄ β Fin β§ π΅ β dom π΄) β (β―β(π΄ βΎ π΅)) = (β―βπ΅)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashreshashfun 14422 | The number of elements of a finite function expressed by a restriction. (Contributed by AV, 15-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((Fun π΄ β§ π΄ β Fin β§ π΅ β dom π΄) β (β―βπ΄) = ((β―β(π΄ βΎ π΅)) + (β―β(dom π΄ β π΅)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashimarn 14423 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((πΈ:dom πΈβ1-1βran πΈ β§ πΈ β π) β (πΉ:(0..^(β―βπΉ))β1-1βdom πΈ β (β―β(πΈ β ran πΉ)) = (β―βπΉ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashimarni 14424 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((πΈ:dom πΈβ1-1βran πΈ β§ πΈ β π) β ((πΉ:(0..^(β―βπΉ))β1-1βdom πΈ β§ π = (πΈ β ran πΉ) β§ (β―βπ) = π) β (β―βπΉ) = π)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfundm 14425 | The size of a set function is equal to the size of its domain. (Contributed by BTernaryTau, 30-Sep-2023.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((πΉ β π β§ Fun πΉ) β (β―βπΉ) = (β―βdom πΉ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashf1dmrn 14426 | The size of the domain of a one-to-one set function is equal to the size of its range. (Contributed by BTernaryTau, 1-Oct-2023.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((πΉ β π β§ πΉ:π΄β1-1βπ΅) β (β―βπ΄) = (β―βran πΉ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashf1dmcdm 14427 | The size of the domain of a one-to-one set function is less than or equal to the size of its codomain, if it exists. (Contributed by BTernaryTau, 1-Oct-2023.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((πΉ β π β§ π΅ β π β§ πΉ:π΄β1-1βπ΅) β (β―βπ΄) β€ (β―βπ΅)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | resunimafz0 14428 | TODO-AV: Revise using πΉ β Word dom πΌ? Formerly part of proof of eupth2lem3 30033: 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β Fun πΌ) & β’ (π β πΉ:(0..^(β―βπΉ))βΆdom πΌ) & β’ (π β π β (0..^(β―βπΉ))) β β’ (π β (πΌ βΎ (πΉ β (0...π))) = ((πΌ βΎ (πΉ β (0..^π))) βͺ {β¨(πΉβπ), (πΌβ(πΉβπ))β©})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fnfz0hash 14429 | The size of a function on a finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 25-Jun-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β β0 β§ πΉ Fn (0...π)) β (β―βπΉ) = (π + 1)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ffz0hash 14430 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β β0 β§ πΉ:(0...π)βΆπ΅) β (β―βπΉ) = (π + 1)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fnfz0hashnn0 14431 | The size of a function on a finite set of sequential nonnegative integers is a nonnegative integer. (Contributed by AV, 10-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (πΉ Fn (0...π) β (β―βπΉ) β β0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ffzo0hash 14432 | The size of a function on a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 25-Mar-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β β0 β§ πΉ Fn (0..^π)) β (β―βπΉ) = π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fnfzo0hash 14433 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β β0 β§ πΉ:(0..^π)βΆπ΅) β (β―βπΉ) = π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fnfzo0hashnn0 14434 | The value of the size function on a half-open range of nonnegative integers is a nonnegative integer. (Contributed by AV, 10-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (πΉ Fn (0..^π) β (β―βπΉ) β β0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashbclem 14435* | Lemma for hashbc 14436: inductive step. (Contributed by Mario Carneiro, 13-Jul-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π΄ β Fin) & β’ (π β Β¬ π§ β π΄) & β’ (π β βπ β β€ ((β―βπ΄)Cπ) = (β―β{π₯ β π« π΄ β£ (β―βπ₯) = π})) & β’ (π β πΎ β β€) β β’ (π β ((β―β(π΄ βͺ {π§}))CπΎ) = (β―β{π₯ β π« (π΄ βͺ {π§}) β£ (β―βπ₯) = πΎ})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashbc 14436* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β Fin β§ πΎ β β€) β ((β―βπ΄)CπΎ) = (β―β{π₯ β π« π΄ β£ (β―βπ₯) = πΎ})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfacen 14437* | The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015.) (Proof shortened by AV, 7-Aug-2024.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β π΅ β§ πΆ β π·) β {π β£ π:π΄β1-1-ontoβπΆ} β {π β£ π:π΅β1-1-ontoβπ·}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfacenOLD 14438* | Obsolete version of hashfacen 14437 as of 7-Aug-2024. (Contributed by Mario Carneiro, 21-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β π΅ β§ πΆ β π·) β {π β£ π:π΄β1-1-ontoβπΆ} β {π β£ π:π΅β1-1-ontoβπ·}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashf1lem1 14439* | Lemma for hashf1 14442. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 14-Aug-2024.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π΄ β Fin) & β’ (π β π΅ β Fin) & β’ (π β Β¬ π§ β π΄) & β’ (π β ((β―βπ΄) + 1) β€ (β―βπ΅)) & β’ (π β πΉ:π΄β1-1βπ΅) β β’ (π β {π β£ ((π βΎ π΄) = πΉ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β (π΅ β ran πΉ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashf1lem1OLD 14440* | Obsolete version of hashf1lem1 14439 as of 7-Aug-2024. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π΄ β Fin) & β’ (π β π΅ β Fin) & β’ (π β Β¬ π§ β π΄) & β’ (π β ((β―βπ΄) + 1) β€ (β―βπ΅)) & β’ (π β πΉ:π΄β1-1βπ΅) β β’ (π β {π β£ ((π βΎ π΄) = πΉ β§ π:(π΄ βͺ {π§})β1-1βπ΅)} β (π΅ β ran πΉ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashf1lem2 14441* | Lemma for hashf1 14442. (Contributed by Mario Carneiro, 17-Apr-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π΄ β Fin) & β’ (π β π΅ β Fin) & β’ (π β Β¬ π§ β π΄) & β’ (π β ((β―βπ΄) + 1) β€ (β―βπ΅)) β β’ (π β (β―β{π β£ π:(π΄ βͺ {π§})β1-1βπ΅}) = (((β―βπ΅) β (β―βπ΄)) Β· (β―β{π β£ π:π΄β1-1βπ΅}))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashf1 14442* | The permutation number β£ π΄ β£ ! Β· ( β£ π΅ β£ C β£ π΄ β£ ) = β£ π΅ β£ ! / ( β£ π΅ β£ β β£ π΄ β£ )! counts the number of injections from π΄ to π΅. (Contributed by Mario Carneiro, 21-Jan-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β Fin β§ π΅ β Fin) β (β―β{π β£ π:π΄β1-1βπ΅}) = ((!β(β―βπ΄)) Β· ((β―βπ΅)C(β―βπ΄)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashfac 14443* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π΄ β Fin β (β―β{π β£ π:π΄β1-1-ontoβπ΄}) = (!β(β―βπ΄))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | leiso 14444 | Two ways to write a strictly increasing function on the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β β* β§ π΅ β β*) β (πΉ Isom < , < (π΄, π΅) β πΉ Isom β€ , β€ (π΄, π΅))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | leisorel 14445 | Version of isorel 7328 for strictly increasing functions on the reals. (Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro, 9-Sep-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((πΉ Isom < , < (π΄, π΅) β§ (π΄ β β* β§ π΅ β β*) β§ (πΆ β π΄ β§ π· β π΄)) β (πΆ β€ π· β (πΉβπΆ) β€ (πΉβπ·))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fz1isolem 14446* | Lemma for fz1iso 14447. (Contributed by Mario Carneiro, 2-Apr-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΊ = (rec((π β V β¦ (π + 1)), 1) βΎ Ο) & β’ π΅ = (β β© (β‘ < β {((β―βπ΄) + 1)})) & β’ πΆ = (Ο β© (β‘πΊβ((β―βπ΄) + 1))) & β’ π = OrdIso(π , π΄) β β’ ((π Or π΄ β§ π΄ β Fin) β βπ π Isom < , π ((1...(β―βπ΄)), π΄)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fz1iso 14447* | Any finite ordered set has an order isomorphism to a one-based finite sequence. (Contributed by Mario Carneiro, 2-Apr-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π Or π΄ β§ π΄ β Fin) β βπ π Isom < , π ((1...(β―βπ΄)), π΄)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ishashinf 14448* | Any set that is not finite contains subsets of arbitrarily large finite cardinality. Cf. isinf 9276. (Contributed by Thierry Arnoux, 5-Jul-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (Β¬ π΄ β Fin β βπ β β βπ₯ β π« π΄(β―βπ₯) = π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | seqcoll 14449* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β§ π β π) β (π + π) = π) & β’ ((π β§ π β π) β (π + π) = π) & β’ ((π β§ (π β π β§ π β π)) β (π + π) β π) & β’ (π β π β π) & β’ (π β πΊ Isom < , < ((1...(β―βπ΄)), π΄)) & β’ (π β π β (1...(β―βπ΄))) & β’ (π β π΄ β (β€β₯βπ)) & β’ ((π β§ π β (π...(πΊβ(β―βπ΄)))) β (πΉβπ) β π) & β’ ((π β§ π β ((π...(πΊβ(β―βπ΄))) β π΄)) β (πΉβπ) = π) & β’ ((π β§ π β (1...(β―βπ΄))) β (π»βπ) = (πΉβ(πΊβπ))) β β’ (π β (seqπ( + , πΉ)β(πΊβπ)) = (seq1( + , π»)βπ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | seqcoll2 14450* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β§ π β π) β (π + π) = π) & β’ ((π β§ π β π) β (π + π) = π) & β’ ((π β§ (π β π β§ π β π)) β (π + π) β π) & β’ (π β π β π) & β’ (π β πΊ Isom < , < ((1...(β―βπ΄)), π΄)) & β’ (π β π΄ β β ) & β’ (π β π΄ β (π...π)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β π) & β’ ((π β§ π β ((π...π) β π΄)) β (πΉβπ) = π) & β’ ((π β§ π β (1...(β―βπ΄))) β (π»βπ) = (πΉβ(πΊβπ))) β β’ (π β (seqπ( + , πΉ)βπ) = (seq1( + , π»)β(β―βπ΄))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | phphashd 14451 | Corollary of the Pigeonhole Principle using equality. Equivalent of phpeqd 9231 expressed using the hash function. (Contributed by Rohan Ridenour, 3-Aug-2023.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π΄ β Fin) & β’ (π β π΅ β π΄) & β’ (π β (β―βπ΄) = (β―βπ΅)) β β’ (π β π΄ = π΅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | phphashrd 14452 | Corollary of the Pigeonhole Principle using equality. Equivalent of phphashd 14451 with reversed arguments. (Contributed by Rohan Ridenour, 3-Aug-2023.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π΅ β Fin) & β’ (π β π΄ β π΅) & β’ (π β (β―βπ΄) = (β―βπ΅)) β β’ (π β π΄ = π΅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashprlei 14453 | An unordered pair has at most two elements. (Contributed by Mario Carneiro, 11-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ({π΄, π΅} β Fin β§ (β―β{π΄, π΅}) β€ 2) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2pr 14454* | A set of size two is an unordered pair. (Contributed by Alexander van der Vekens, 8-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β π β§ (β―βπ) = 2) β βπβπ π = {π, π}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2prde 14455* | A set of size two is an unordered pair of two different elements. (Contributed by Alexander van der Vekens, 8-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β π β§ (β―βπ) = 2) β βπβπ(π β π β§ π = {π, π})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2exprb 14456* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π β ((β―βπ) = 2 β βπβπ(π β π β§ π = {π, π}))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2prb 14457* | A set of size two is a proper unordered pair. (Contributed by AV, 1-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π β ((β―βπ) = 2 β βπ β π βπ β π (π β π β§ π = {π, π}))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | prprrab 14458 | The set of proper pairs of elements of a given set expressed in two ways. (Contributed by AV, 24-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ {π₯ β (π« π΄ β {β }) β£ (β―βπ₯) = 2} = {π₯ β π« π΄ β£ (β―βπ₯) = 2} | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nehash2 14459 | The cardinality of a set with two distinct elements. (Contributed by Thierry Arnoux, 27-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π΄ β π΅) β β’ (π β 2 β€ (β―βπ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2prd 14460 | 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, 16-Jun-2022.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β π β§ (β―βπ) = 2) β ((π β π β§ π β π β§ π β π) β π = {π, π})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2pwpr 14461 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (((β―βπ) = 2 β§ π β π« {π, π}) β π = {π, π}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashle2pr 14462* | A nonempty set of size less than or equal to two is an unordered pair of sets. (Contributed by AV, 24-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β π β§ π β β ) β ((β―βπ) β€ 2 β βπβπ π = {π, π})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashle2prv 14463* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β (π« π β {β }) β ((β―βπ) β€ 2 β βπ β π βπ β π π = {π, π})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pr2pwpr 14464* | The set of subsets of a pair having length 2 is the set of the pair as singleton. (Contributed by AV, 9-Dec-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β π β§ π΅ β π β§ π΄ β π΅) β {π β π« {π΄, π΅} β£ π β 2o} = {{π΄, π΅}}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashge2el2dif 14465* | A set with size at least 2 has at least 2 different elements. (Contributed by AV, 18-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π· β π β§ 2 β€ (β―βπ·)) β βπ₯ β π· βπ¦ β π· π₯ β π¦) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashge2el2difr 14466* | A set with at least 2 different elements has size at least 2. (Contributed by AV, 14-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π· β π β§ βπ₯ β π· βπ¦ β π· π₯ β π¦) β 2 β€ (β―βπ·)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashge2el2difb 14467* | A set has size at least 2 iff it has at least 2 different elements. (Contributed by AV, 14-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π· β π β (2 β€ (β―βπ·) β βπ₯ β π· βπ¦ β π· π₯ β π¦)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashdmpropge2 14468 | The size of the domain of a class which contains two ordered pairs with different first components is greater than or equal to 2. (Contributed by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β πΉ β π) & β’ (π β π΄ β π΅) & β’ (π β {β¨π΄, πΆβ©, β¨π΅, π·β©} β πΉ) β β’ (π β 2 β€ (β―βdom πΉ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashtplei 14469 | An unordered triple has at most three elements. (Contributed by Mario Carneiro, 11-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ({π΄, π΅, πΆ} β Fin β§ (β―β{π΄, π΅, πΆ}) β€ 3) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashtpg 14470 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β ((π΄ β π΅ β§ π΅ β πΆ β§ πΆ β π΄) β (β―β{π΄, π΅, πΆ}) = 3)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashge3el3dif 14471* | A set with size at least 3 has at least 3 different elements. In contrast to hashge2el2dif 14465, 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π· β π β§ 3 β€ (β―βπ·)) β βπ₯ β π· βπ¦ β π· βπ§ β π· (π₯ β π¦ β§ π₯ β π§ β§ π¦ β π§)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | elss2prb 14472* | An element of the set of subsets with two elements is a proper unordered pair. (Contributed by AV, 1-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β {π§ β π« π β£ (β―βπ§) = 2} β βπ₯ β π βπ¦ β π (π₯ β π¦ β§ π = {π₯, π¦})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash2sspr 14473* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β π« π β§ (β―βπ) = 2) β βπ β π βπ β π π = {π, π}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | exprelprel 14474* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (βπ β {π β π« π β£ (β―βπ) = 2}π β π β βπ£ β π βπ€ β π {π£, π€} β π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash3tr 14475* | A set of size three is an unordered triple. (Contributed by Alexander van der Vekens, 13-Sep-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β π β§ (β―βπ) = 3) β βπβπβπ π = {π, π, π}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hash1to3 14476* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β Fin β§ 1 β€ (β―βπ) β§ (β―βπ) β€ 3) β βπβπβπ(π = {π} β¨ π = {π, π} β¨ π = {π, π, π})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fundmge2nop0 14477 | A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fundmge2nop 14478 (with the less restrictive requirement that (πΊ β {β }) needs to be a function instead of πΊ) is useful for proofs for extensible structures, see structn0fun 17111. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 7-Jun-2021.) (Proof shortened by AV, 15-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((Fun (πΊ β {β }) β§ 2 β€ (β―βdom πΊ)) β Β¬ πΊ β (V Γ V)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fundmge2nop 14478 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((Fun πΊ β§ 2 β€ (β―βdom πΊ)) β Β¬ πΊ β (V Γ V)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fun2dmnop0 14479 | A function with a domain containing (at least) two different elements is not an ordered pair. This stronger version of fun2dmnop 14480 (with the less restrictive requirement that (πΊ β {β }) needs to be a function instead of πΊ) is useful for proofs for extensible structures, see structn0fun 17111. (Contributed by AV, 21-Sep-2020.) (Revised by AV, 7-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ β V & β’ π΅ β V β β’ ((Fun (πΊ β {β }) β§ π΄ β π΅ β§ {π΄, π΅} β dom πΊ) β Β¬ πΊ β (V Γ V)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fun2dmnop 14480 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π΄ β V & β’ π΅ β V β β’ ((Fun πΊ β§ π΄ β π΅ β§ {π΄, π΅} β dom πΊ) β Β¬ πΊ β (V Γ V)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | hashdifsnp1 14481 | If the size of a set is a nonnegative integer increased by 1, the size of the set with one of its elements removed is this nonnegative integer. (Contributed by Alexander van der Vekens, 7-Jan-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β π β§ π β π β§ π β β0) β ((β―βπ) = (π + 1) β (β―β(π β {π})) = π)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fi1uzind 14482* | 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 πΏ = 0 (see opfi1ind 14487) or πΏ = 1. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΉ β V & β’ πΏ β β0 & β’ ((π£ = π β§ π = πΈ) β (π β π)) & β’ ((π£ = π€ β§ π = π) β (π β π)) & β’ (([π£ / π][π / π]π β§ π β π£) β [(π£ β {π}) / π][πΉ / π]π) & β’ ((π€ = (π£ β {π}) β§ π = πΉ) β (π β π)) & β’ (([π£ / π][π / π]π β§ (β―βπ£) = πΏ) β π) & β’ ((((π¦ + 1) β β0 β§ ([π£ / π][π / π]π β§ (β―βπ£) = (π¦ + 1) β§ π β π£)) β§ π) β π) β β’ (([π / π][πΈ / π]π β§ π β Fin β§ πΏ β€ (β―βπ)) β π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1uzind 14483* | 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 πΏ = 0 (see brfi1ind 14484) or πΏ = 1. (Contributed by Alexander van der Vekens, 7-Jan-2018.) (Proof shortened by AV, 23-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ Rel πΊ & β’ πΉ β V & β’ πΏ β β0 & β’ ((π£ = π β§ π = πΈ) β (π β π)) & β’ ((π£ = π€ β§ π = π) β (π β π)) & β’ ((π£πΊπ β§ π β π£) β (π£ β {π})πΊπΉ) & β’ ((π€ = (π£ β {π}) β§ π = πΉ) β (π β π)) & β’ ((π£πΊπ β§ (β―βπ£) = πΏ) β π) & β’ ((((π¦ + 1) β β0 β§ (π£πΊπ β§ (β―βπ£) = (π¦ + 1) β§ π β π£)) β§ π) β π) β β’ ((ππΊπΈ β§ π β Fin β§ πΏ β€ (β―βπ)) β π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1ind 14484* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ Rel πΊ & β’ πΉ β V & β’ ((π£ = π β§ π = πΈ) β (π β π)) & β’ ((π£ = π€ β§ π = π) β (π β π)) & β’ ((π£πΊπ β§ π β π£) β (π£ β {π})πΊπΉ) & β’ ((π€ = (π£ β {π}) β§ π = πΉ) β (π β π)) & β’ ((π£πΊπ β§ (β―βπ£) = 0) β π) & β’ ((((π¦ + 1) β β0 β§ (π£πΊπ β§ (β―βπ£) = (π¦ + 1) β§ π β π£)) β§ π) β π) β β’ ((ππΊπΈ β§ π β Fin) β π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brfi1indALT 14485* | Alternate proof of brfi1ind 14484, which does not use brfi1uzind 14483. (Contributed by Alexander van der Vekens, 7-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ Rel πΊ & β’ πΉ β V & β’ ((π£ = π β§ π = πΈ) β (π β π)) & β’ ((π£ = π€ β§ π = π) β (π β π)) & β’ ((π£πΊπ β§ π β π£) β (π£ β {π})πΊπΉ) & β’ ((π€ = (π£ β {π}) β§ π = πΉ) β (π β π)) & β’ ((π£πΊπ β§ (β―βπ£) = 0) β π) & β’ ((((π¦ + 1) β β0 β§ (π£πΊπ β§ (β―βπ£) = (π¦ + 1) β§ π β π£)) β§ π) β π) β β’ ((ππΊπΈ β§ π β Fin) β π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opfi1uzind 14486* | 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 πΏ = 0 (see opfi1ind 14487) or πΏ = 1. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΈ β V & β’ πΉ β V & β’ πΏ β β0 & β’ ((π£ = π β§ π = πΈ) β (π β π)) & β’ ((π£ = π€ β§ π = π) β (π β π)) & β’ ((β¨π£, πβ© β πΊ β§ π β π£) β β¨(π£ β {π}), πΉβ© β πΊ) & β’ ((π€ = (π£ β {π}) β§ π = πΉ) β (π β π)) & β’ ((β¨π£, πβ© β πΊ β§ (β―βπ£) = πΏ) β π) & β’ ((((π¦ + 1) β β0 β§ (β¨π£, πβ© β πΊ β§ (β―βπ£) = (π¦ + 1) β§ π β π£)) β§ π) β π) β β’ ((β¨π, πΈβ© β πΊ β§ π β Fin β§ πΏ β€ (β―βπ)) β π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opfi1ind 14487* | 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 29130. (Contributed by AV, 22-Oct-2020.) (Revised by AV, 28-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ πΈ β V & β’ πΉ β V & β’ ((π£ = π β§ π = πΈ) β (π β π)) & β’ ((π£ = π€ β§ π = π) β (π β π)) & β’ ((β¨π£, πβ© β πΊ β§ π β π£) β β¨(π£ β {π}), πΉβ© β πΊ) & β’ ((π€ = (π£ β {π}) β§ π = πΉ) β (π β π)) & β’ ((β¨π£, πβ© β πΊ β§ (β―βπ£) = 0) β π) & β’ ((((π¦ + 1) β β0 β§ (β¨π£, πβ© β πΊ β§ (β―βπ£) = (π¦ + 1) β§ π β π£)) β§ π) β π) β β’ ((β¨π, πΈβ© β πΊ β§ π β Fin) β π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
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 14489, see, for example, s1cli 14579: β¨βπ΄ββ© β Word V. Note that the empty word β (i.e., the empty set) is the only word over an empty alphabet, see 0wrd0 14514. 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 14488 | Syntax for the Word operator. | ||||||||||||||||||||||||||||||||||||||||||||||||||
class Word π | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-word 14489* | 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 β0 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 π equipped with concatenation is the free monoid over π, and the monoid unit is the empty word (see frmdval 18794). (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 14-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ Word π = {π€ β£ βπ β β0 π€:(0..^π)βΆπ} | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iswrd 14490* | Property of being a word over a set with an existential quantifier over the length. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 13-May-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β Word π β βπ β β0 π:(0..^π)βΆπ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdval 14491* | Value of the set of words over a set. (Contributed by Stefan O'Rear, 10-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π β Word π = βͺ π β β0 (π βm (0..^π))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iswrdi 14492 | A zero-based sequence is a word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π:(0..^πΏ)βΆπ β π β Word π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdf 14493 | A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β Word π β π:(0..^(β―βπ))βΆπ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iswrdb 14494 | A word over an alphabet is a function from an open range of nonnegative integers (of length equal to the length of the word) into the alphabet. (Contributed by Alexander van der Vekens, 30-Jul-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β Word π β π:(0..^(β―βπ))βΆπ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrddm 14495 | The indices of a word (i.e. its domain regarded as function) are elements of an open range of nonnegative integers (of length equal to the length of the word). (Contributed by AV, 2-May-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β Word π β dom π = (0..^(β―βπ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sswrd 14496 | The set of words respects ordering on the base set. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 13-May-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π β Word π β Word π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | snopiswrd 14497 | A singleton of an ordered pair (with 0 as first component) is a word. (Contributed by AV, 23-Nov-2018.) (Proof shortened by AV, 18-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π β {β¨0, πβ©} β Word π) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdexg 14498 | The set of words over a set is a set. (Contributed by Mario Carneiro, 26-Feb-2016.) (Proof shortened by JJ, 18-Nov-2022.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π β Word π β V) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdexb 14499 | The set of words over a set is a set, bidirectional version. (Contributed by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 23-Nov-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β V β Word π β V) | ||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdexi 14500 | The set of words over a set is a set, inference form. (Contributed by AV, 23-May-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π β V β β’ Word π β V |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |