![]() |
Metamath
Proof Explorer Theorem List (p. 95 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fsuppcor 9401 | The composition of a function which maps the zero of the range of a finitely supported function to the zero of its range with this finitely supported function is finitely supported. (Contributed by AV, 6-Jun-2019.) |
β’ (π β 0 β π) & β’ (π β π β π΅) & β’ (π β πΉ:π΄βΆπΆ) & β’ (π β πΊ:π΅βΆπ·) & β’ (π β πΆ β π΅) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΉ finSupp π) & β’ (π β (πΊβπ) = 0 ) β β’ (π β (πΊ β πΉ) finSupp 0 ) | ||
Theorem | mapfienlem1 9402* | Lemma 1 for mapfien 9405. (Contributed by AV, 3-Jul-2019.) (Revised by AV, 28-Jul-2024.) |
β’ π = {π₯ β (π΅ βm π΄) β£ π₯ finSupp π} & β’ π = {π₯ β (π· βm πΆ) β£ π₯ finSupp π} & β’ π = (πΊβπ) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄) & β’ (π β πΊ:π΅β1-1-ontoβπ·) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π β π΅) β β’ ((π β§ π β π) β (πΊ β (π β πΉ)) finSupp π) | ||
Theorem | mapfienlem2 9403* | Lemma 2 for mapfien 9405. (Contributed by AV, 3-Jul-2019.) (Revised by AV, 28-Jul-2024.) |
β’ π = {π₯ β (π΅ βm π΄) β£ π₯ finSupp π} & β’ π = {π₯ β (π· βm πΆ) β£ π₯ finSupp π} & β’ π = (πΊβπ) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄) & β’ (π β πΊ:π΅β1-1-ontoβπ·) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π β π΅) β β’ ((π β§ π β π) β ((β‘πΊ β π) β β‘πΉ) finSupp π) | ||
Theorem | mapfienlem3 9404* | Lemma 3 for mapfien 9405. (Contributed by AV, 3-Jul-2019.) (Revised by AV, 28-Jul-2024.) |
β’ π = {π₯ β (π΅ βm π΄) β£ π₯ finSupp π} & β’ π = {π₯ β (π· βm πΆ) β£ π₯ finSupp π} & β’ π = (πΊβπ) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄) & β’ (π β πΊ:π΅β1-1-ontoβπ·) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π β π΅) β β’ ((π β§ π β π) β ((β‘πΊ β π) β β‘πΉ) β π) | ||
Theorem | mapfien 9405* | A bijection of the base sets induces a bijection on the set of finitely supported functions. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 3-Jul-2019.) (Revised by AV, 28-Jul-2024.) |
β’ π = {π₯ β (π΅ βm π΄) β£ π₯ finSupp π} & β’ π = {π₯ β (π· βm πΆ) β£ π₯ finSupp π} & β’ π = (πΊβπ) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄) & β’ (π β πΊ:π΅β1-1-ontoβπ·) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π β π΅) β β’ (π β (π β π β¦ (πΊ β (π β πΉ))):πβ1-1-ontoβπ) | ||
Theorem | mapfien2 9406* | Equinumerousity relation for sets of finitely supported functions. (Contributed by Stefan O'Rear, 9-Jul-2015.) (Revised by AV, 7-Jul-2019.) |
β’ π = {π₯ β (π΅ βm π΄) β£ π₯ finSupp 0 } & β’ π = {π₯ β (π· βm πΆ) β£ π₯ finSupp π} & β’ (π β π΄ β πΆ) & β’ (π β π΅ β π·) & β’ (π β 0 β π΅) & β’ (π β π β π·) β β’ (π β π β π) | ||
Syntax | cfi 9407 | Extend class notation with the function whose value is the class of finite intersections of the elements of a given set. |
class fi | ||
Definition | df-fi 9408* | Function whose value is the class of finite intersections of the elements of the argument. Note that the empty intersection being the universal class, hence a proper class, it cannot be an element of that class. Therefore, the function value is the class of nonempty finite intersections of elements of the argument (see elfi2 9411). (Contributed by FL, 27-Apr-2008.) |
β’ fi = (π₯ β V β¦ {π§ β£ βπ¦ β (π« π₯ β© Fin)π§ = β© π¦}) | ||
Theorem | fival 9409* | The set of all the finite intersections of the elements of π΄. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
β’ (π΄ β π β (fiβπ΄) = {π¦ β£ βπ₯ β (π« π΄ β© Fin)π¦ = β© π₯}) | ||
Theorem | elfi 9410* | Specific properties of an element of (fiβπ΅). (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄ β (fiβπ΅) β βπ₯ β (π« π΅ β© Fin)π΄ = β© π₯)) | ||
Theorem | elfi2 9411* | The empty intersection need not be considered in the set of finite intersections. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ (π΅ β π β (π΄ β (fiβπ΅) β βπ₯ β ((π« π΅ β© Fin) β {β })π΄ = β© π₯)) | ||
Theorem | elfir 9412 | Sufficient condition for an element of (fiβπ΅). (Contributed by Mario Carneiro, 24-Nov-2013.) |
β’ ((π΅ β π β§ (π΄ β π΅ β§ π΄ β β β§ π΄ β Fin)) β β© π΄ β (fiβπ΅)) | ||
Theorem | intrnfi 9413 | Sufficient condition for the intersection of the range of a function to be in the set of finite intersections. (Contributed by Mario Carneiro, 30-Aug-2015.) |
β’ ((π΅ β π β§ (πΉ:π΄βΆπ΅ β§ π΄ β β β§ π΄ β Fin)) β β© ran πΉ β (fiβπ΅)) | ||
Theorem | iinfi 9414* | An indexed intersection of elements of πΆ is an element of the finite intersections of πΆ. (Contributed by Mario Carneiro, 30-Aug-2015.) |
β’ ((πΆ β π β§ (βπ₯ β π΄ π΅ β πΆ β§ π΄ β β β§ π΄ β Fin)) β β© π₯ β π΄ π΅ β (fiβπΆ)) | ||
Theorem | inelfi 9415 | The intersection of two sets is a finite intersection. (Contributed by Thierry Arnoux, 6-Jan-2017.) |
β’ ((π β π β§ π΄ β π β§ π΅ β π) β (π΄ β© π΅) β (fiβπ)) | ||
Theorem | ssfii 9416 | Any element of a set π΄ is the intersection of a finite subset of π΄. (Contributed by FL, 27-Apr-2008.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
β’ (π΄ β π β π΄ β (fiβπ΄)) | ||
Theorem | fi0 9417 | The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.) |
β’ (fiββ ) = β | ||
Theorem | fieq0 9418 | A set is empty iff the class of all the finite intersections of that set is empty. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
β’ (π΄ β π β (π΄ = β β (fiβπ΄) = β )) | ||
Theorem | fiin 9419 | The elements of (fiβπΆ) are closed under finite intersection. (Contributed by Mario Carneiro, 24-Nov-2013.) |
β’ ((π΄ β (fiβπΆ) β§ π΅ β (fiβπΆ)) β (π΄ β© π΅) β (fiβπΆ)) | ||
Theorem | dffi2 9420* | The set of finite intersections is the smallest set that contains π΄ and is closed under pairwise intersection. (Contributed by Mario Carneiro, 24-Nov-2013.) |
β’ (π΄ β π β (fiβπ΄) = β© {π§ β£ (π΄ β π§ β§ βπ₯ β π§ βπ¦ β π§ (π₯ β© π¦) β π§)}) | ||
Theorem | fiss 9421 | Subset relationship for function fi. (Contributed by Jeff Hankins, 7-Oct-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
β’ ((π΅ β π β§ π΄ β π΅) β (fiβπ΄) β (fiβπ΅)) | ||
Theorem | inficl 9422* | A set which is closed under pairwise intersection is closed under finite intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
β’ (π΄ β π β (βπ₯ β π΄ βπ¦ β π΄ (π₯ β© π¦) β π΄ β (fiβπ΄) = π΄)) | ||
Theorem | fipwuni 9423 | The set of finite intersections of a set is contained in the powerset of the union of the elements of π΄. (Contributed by Mario Carneiro, 24-Nov-2013.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
β’ (fiβπ΄) β π« βͺ π΄ | ||
Theorem | fisn 9424 | A singleton is closed under finite intersections. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (fiβ{π΄}) = {π΄} | ||
Theorem | fiuni 9425 | The union of the finite intersections of a set is simply the union of the set itself. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
β’ (π΄ β π β βͺ π΄ = βͺ (fiβπ΄)) | ||
Theorem | fipwss 9426 | If a set is a family of subsets of some base set, then so is its finite intersection. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
β’ (π΄ β π« π β (fiβπ΄) β π« π) | ||
Theorem | elfiun 9427* | A finite intersection of elements taken from a union of collections. (Contributed by Jeff Hankins, 15-Nov-2009.) (Proof shortened by Mario Carneiro, 26-Nov-2013.) |
β’ ((π΅ β π· β§ πΆ β πΎ) β (π΄ β (fiβ(π΅ βͺ πΆ)) β (π΄ β (fiβπ΅) β¨ π΄ β (fiβπΆ) β¨ βπ₯ β (fiβπ΅)βπ¦ β (fiβπΆ)π΄ = (π₯ β© π¦)))) | ||
Theorem | dffi3 9428* | The set of finite intersections can be "constructed" inductively by iterating binary intersection Ο-many times. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ π = (π’ β V β¦ ran (π¦ β π’, π§ β π’ β¦ (π¦ β© π§))) β β’ (π΄ β π β (fiβπ΄) = βͺ (rec(π , π΄) β Ο)) | ||
Theorem | fifo 9429* | Describe a surjection from nonempty finite sets to finite intersections. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ πΉ = (π¦ β ((π« π΄ β© Fin) β {β }) β¦ β© π¦) β β’ (π΄ β π β πΉ:((π« π΄ β© Fin) β {β })βontoβ(fiβπ΄)) | ||
Theorem | marypha1lem 9430* | Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015.) |
β’ (π΄ β Fin β (π β Fin β βπ β π« (π΄ Γ π)(βπ β π« π΄π βΌ (π β π) β βπ β π« ππ:π΄β1-1βV))) | ||
Theorem | marypha1 9431* | (Philip) Hall's marriage theorem, sufficiency: a finite relation contains an injection if there is no subset of its domain which would be forced to violate the pigeonhole principle. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
β’ (π β π΄ β Fin) & β’ (π β π΅ β Fin) & β’ (π β πΆ β (π΄ Γ π΅)) & β’ ((π β§ π β π΄) β π βΌ (πΆ β π)) β β’ (π β βπ β π« πΆπ:π΄β1-1βπ΅) | ||
Theorem | marypha2lem1 9432* | Lemma for marypha2 9436. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
β’ π = βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β β’ π β (π΄ Γ βͺ ran πΉ) | ||
Theorem | marypha2lem2 9433* | Lemma for marypha2 9436. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
β’ π = βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β β’ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πΉβπ₯))} | ||
Theorem | marypha2lem3 9434* | Lemma for marypha2 9436. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
β’ π = βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β β’ ((πΉ Fn π΄ β§ πΊ Fn π΄) β (πΊ β π β βπ₯ β π΄ (πΊβπ₯) β (πΉβπ₯))) | ||
Theorem | marypha2lem4 9435* | Lemma for marypha2 9436. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
β’ π = βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β β’ ((πΉ Fn π΄ β§ π β π΄) β (π β π) = βͺ (πΉ β π)) | ||
Theorem | marypha2 9436* | Version of marypha1 9431 using a functional family of sets instead of a relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
β’ (π β π΄ β Fin) & β’ (π β πΉ:π΄βΆFin) & β’ ((π β§ π β π΄) β π βΌ βͺ (πΉ β π)) β β’ (π β βπ(π:π΄β1-1βV β§ βπ₯ β π΄ (πβπ₯) β (πΉβπ₯))) | ||
Syntax | csup 9437 | Extend class notation to include supremum of class π΄. Here π is ordinarily a relation that strictly orders class π΅. For example, π could be 'less than' and π΅ could be the set of real numbers. |
class sup(π΄, π΅, π ) | ||
Syntax | cinf 9438 | Extend class notation to include infimum of class π΄. Here π is ordinarily a relation that strictly orders class π΅. For example, π could be 'less than' and π΅ could be the set of real numbers. |
class inf(π΄, π΅, π ) | ||
Definition | df-sup 9439* | Define the supremum of class π΄. It is meaningful when π is a relation that strictly orders π΅ and when the supremum exists. For example, π could be 'less than', π΅ could be the set of real numbers, and π΄ could be the set of all positive reals whose square is less than 2; in this case the supremum is defined as the square root of 2 per sqrtval 15188. See dfsup2 9441 for alternate definition not requiring dummy variables. (Contributed by NM, 22-May-1999.) |
β’ sup(π΄, π΅, π ) = βͺ {π₯ β π΅ β£ (βπ¦ β π΄ Β¬ π₯π π¦ β§ βπ¦ β π΅ (π¦π π₯ β βπ§ β π΄ π¦π π§))} | ||
Definition | df-inf 9440 | Define the infimum of class π΄. It is meaningful when π is a relation that strictly orders π΅ and when the infimum exists. For example, π could be 'less than', π΅ could be the set of real numbers, and π΄ could be the set of all positive reals; in this case the infimum is 0. The infimum is defined as the supremum using the converse ordering relation. In the given example, 0 is the supremum of all reals (greatest real number) for which all positive reals are greater. (Contributed by AV, 2-Sep-2020.) |
β’ inf(π΄, π΅, π ) = sup(π΄, π΅, β‘π ) | ||
Theorem | dfsup2 9441 | Quantifier-free definition of supremum. (Contributed by Scott Fenton, 19-Feb-2013.) |
β’ sup(π΅, π΄, π ) = βͺ (π΄ β ((β‘π β π΅) βͺ (π β (π΄ β (β‘π β π΅))))) | ||
Theorem | supeq1 9442 | Equality theorem for supremum. (Contributed by NM, 22-May-1999.) |
β’ (π΅ = πΆ β sup(π΅, π΄, π ) = sup(πΆ, π΄, π )) | ||
Theorem | supeq1d 9443 | Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ (π β π΅ = πΆ) β β’ (π β sup(π΅, π΄, π ) = sup(πΆ, π΄, π )) | ||
Theorem | supeq1i 9444 | Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ π΅ = πΆ β β’ sup(π΅, π΄, π ) = sup(πΆ, π΄, π ) | ||
Theorem | supeq2 9445 | Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π΅ = πΆ β sup(π΄, π΅, π ) = sup(π΄, πΆ, π )) | ||
Theorem | supeq3 9446 | Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.) |
β’ (π = π β sup(π΄, π΅, π ) = sup(π΄, π΅, π)) | ||
Theorem | supeq123d 9447 | Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
β’ (π β π΄ = π·) & β’ (π β π΅ = πΈ) & β’ (π β πΆ = πΉ) β β’ (π β sup(π΄, π΅, πΆ) = sup(π·, πΈ, πΉ)) | ||
Theorem | nfsup 9448 | Hypothesis builder for supremum. (Contributed by Mario Carneiro, 20-Mar-2014.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π β β’ β²π₯sup(π΄, π΅, π ) | ||
Theorem | supmo 9449* | Any class π΅ has at most one supremum in π΄ (where π is interpreted as 'less than'). (Contributed by NM, 5-May-1999.) (Revised by Mario Carneiro, 24-Dec-2016.) |
β’ (π β π Or π΄) β β’ (π β β*π₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) | ||
Theorem | supexd 9450 | A supremum is a set. (Contributed by NM, 22-May-1999.) (Revised by Mario Carneiro, 24-Dec-2016.) |
β’ (π β π Or π΄) β β’ (π β sup(π΅, π΄, π ) β V) | ||
Theorem | supeu 9451* | A supremum is unique. Similar to Theorem I.26 of [Apostol] p. 24 (but for suprema in general). (Contributed by NM, 12-Oct-2004.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β β!π₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) | ||
Theorem | supval2 9452* | Alternate expression for the supremum. (Contributed by Mario Carneiro, 24-Dec-2016.) (Revised by Thierry Arnoux, 24-Sep-2017.) |
β’ (π β π Or π΄) β β’ (π β sup(π΅, π΄, π ) = (β©π₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§)))) | ||
Theorem | eqsup 9453* | Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015.) |
β’ (π β π Or π΄) β β’ (π β ((πΆ β π΄ β§ βπ¦ β π΅ Β¬ πΆπ π¦ β§ βπ¦ β π΄ (π¦π πΆ β βπ§ β π΅ π¦π π§)) β sup(π΅, π΄, π ) = πΆ)) | ||
Theorem | eqsupd 9454* | Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015.) |
β’ (π β π Or π΄) & β’ (π β πΆ β π΄) & β’ ((π β§ π¦ β π΅) β Β¬ πΆπ π¦) & β’ ((π β§ (π¦ β π΄ β§ π¦π πΆ)) β βπ§ β π΅ π¦π π§) β β’ (π β sup(π΅, π΄, π ) = πΆ) | ||
Theorem | supcl 9455* | A supremum belongs to its base class (closure law). See also supub 9456 and suplub 9457. (Contributed by NM, 12-Oct-2004.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β sup(π΅, π΄, π ) β π΄) | ||
Theorem | supub 9456* |
A supremum is an upper bound. See also supcl 9455 and suplub 9457.
This proof demonstrates how to expand an iota-based definition (df-iota 6494) using riotacl2 7384. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β (πΆ β π΅ β Β¬ sup(π΅, π΄, π )π πΆ)) | ||
Theorem | suplub 9457* | A supremum is the least upper bound. See also supcl 9455 and supub 9456. (Contributed by NM, 13-Oct-2004.) (Revised by Mario Carneiro, 24-Dec-2016.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β ((πΆ β π΄ β§ πΆπ sup(π΅, π΄, π )) β βπ§ β π΅ πΆπ π§)) | ||
Theorem | suplub2 9458* | Bidirectional form of suplub 9457. (Contributed by Mario Carneiro, 6-Sep-2014.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) & β’ (π β π΅ β π΄) β β’ ((π β§ πΆ β π΄) β (πΆπ sup(π΅, π΄, π ) β βπ§ β π΅ πΆπ π§)) | ||
Theorem | supnub 9459* | An upper bound is not less than the supremum. (Contributed by NM, 13-Oct-2004.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β ((πΆ β π΄ β§ βπ§ β π΅ Β¬ πΆπ π§) β Β¬ πΆπ sup(π΅, π΄, π ))) | ||
Theorem | supex 9460 | A supremum is a set. (Contributed by NM, 22-May-1999.) |
β’ π Or π΄ β β’ sup(π΅, π΄, π ) β V | ||
Theorem | sup00 9461 | The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
β’ sup(π΅, β , π ) = β | ||
Theorem | sup0riota 9462* | The supremum of an empty set is the smallest element of the base set. (Contributed by AV, 4-Sep-2020.) |
β’ (π Or π΄ β sup(β , π΄, π ) = (β©π₯ β π΄ βπ¦ β π΄ Β¬ π¦π π₯)) | ||
Theorem | sup0 9463* | The supremum of an empty set under a base set which has a unique smallest element is the smallest element of the base set. (Contributed by AV, 4-Sep-2020.) |
β’ ((π Or π΄ β§ (π β π΄ β§ βπ¦ β π΄ Β¬ π¦π π) β§ β!π₯ β π΄ βπ¦ β π΄ Β¬ π¦π π₯) β sup(β , π΄, π ) = π) | ||
Theorem | supmax 9464* | The greatest element of a set is its supremum. Note that the converse is not true; the supremum might not be an element of the set considered. (Contributed by Jeff Hoffman, 17-Jun-2008.) (Proof shortened by OpenAI, 30-Mar-2020.) |
β’ (π β π Or π΄) & β’ (π β πΆ β π΄) & β’ (π β πΆ β π΅) & β’ ((π β§ π¦ β π΅) β Β¬ πΆπ π¦) β β’ (π β sup(π΅, π΄, π ) = πΆ) | ||
Theorem | fisup2g 9465* | A finite set satisfies the conditions to have a supremum. (Contributed by Mario Carneiro, 28-Apr-2015.) |
β’ ((π Or π΄ β§ (π΅ β Fin β§ π΅ β β β§ π΅ β π΄)) β βπ₯ β π΅ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) | ||
Theorem | fisupcl 9466 | A nonempty finite set contains its supremum. (Contributed by Jeff Madsen, 9-May-2011.) |
β’ ((π Or π΄ β§ (π΅ β Fin β§ π΅ β β β§ π΅ β π΄)) β sup(π΅, π΄, π ) β π΅) | ||
Theorem | supgtoreq 9467 | The supremum of a finite set is greater than or equal to all the elements of the set. (Contributed by AV, 1-Oct-2019.) |
β’ (π β π Or π΄) & β’ (π β π΅ β π΄) & β’ (π β π΅ β Fin) & β’ (π β πΆ β π΅) & β’ (π β π = sup(π΅, π΄, π )) β β’ (π β (πΆπ π β¨ πΆ = π)) | ||
Theorem | suppr 9468 | The supremum of a pair. (Contributed by NM, 17-Jun-2007.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
β’ ((π Or π΄ β§ π΅ β π΄ β§ πΆ β π΄) β sup({π΅, πΆ}, π΄, π ) = if(πΆπ π΅, π΅, πΆ)) | ||
Theorem | supsn 9469 | The supremum of a singleton. (Contributed by NM, 2-Oct-2007.) |
β’ ((π Or π΄ β§ π΅ β π΄) β sup({π΅}, π΄, π ) = π΅) | ||
Theorem | supisolem 9470* | Lemma for supiso 9472. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ (π β πΉ Isom π , π (π΄, π΅)) & β’ (π β πΆ β π΄) β β’ ((π β§ π· β π΄) β ((βπ¦ β πΆ Β¬ π·π π¦ β§ βπ¦ β π΄ (π¦π π· β βπ§ β πΆ π¦π π§)) β (βπ€ β (πΉ β πΆ) Β¬ (πΉβπ·)ππ€ β§ βπ€ β π΅ (π€π(πΉβπ·) β βπ£ β (πΉ β πΆ)π€ππ£)))) | ||
Theorem | supisoex 9471* | Lemma for supiso 9472. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ (π β πΉ Isom π , π (π΄, π΅)) & β’ (π β πΆ β π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β πΆ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β πΆ π¦π π§))) β β’ (π β βπ’ β π΅ (βπ€ β (πΉ β πΆ) Β¬ π’ππ€ β§ βπ€ β π΅ (π€ππ’ β βπ£ β (πΉ β πΆ)π€ππ£))) | ||
Theorem | supiso 9472* | Image of a supremum under an isomorphism. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ (π β πΉ Isom π , π (π΄, π΅)) & β’ (π β πΆ β π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β πΆ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β πΆ π¦π π§))) & β’ (π β π Or π΄) β β’ (π β sup((πΉ β πΆ), π΅, π) = (πΉβsup(πΆ, π΄, π ))) | ||
Theorem | infeq1 9473 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π΅ = πΆ β inf(π΅, π΄, π ) = inf(πΆ, π΄, π )) | ||
Theorem | infeq1d 9474 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π β π΅ = πΆ) β β’ (π β inf(π΅, π΄, π ) = inf(πΆ, π΄, π )) | ||
Theorem | infeq1i 9475 | Equality inference for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ π΅ = πΆ β β’ inf(π΅, π΄, π ) = inf(πΆ, π΄, π ) | ||
Theorem | infeq2 9476 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π΅ = πΆ β inf(π΄, π΅, π ) = inf(π΄, πΆ, π )) | ||
Theorem | infeq3 9477 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π = π β inf(π΄, π΅, π ) = inf(π΄, π΅, π)) | ||
Theorem | infeq123d 9478 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π β π΄ = π·) & β’ (π β π΅ = πΈ) & β’ (π β πΆ = πΉ) β β’ (π β inf(π΄, π΅, πΆ) = inf(π·, πΈ, πΉ)) | ||
Theorem | nfinf 9479 | Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π β β’ β²π₯inf(π΄, π΅, π ) | ||
Theorem | infexd 9480 | An infimum is a set. (Contributed by AV, 2-Sep-2020.) |
β’ (π β π Or π΄) β β’ (π β inf(π΅, π΄, π ) β V) | ||
Theorem | eqinf 9481* | Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π β π Or π΄) β β’ (π β ((πΆ β π΄ β§ βπ¦ β π΅ Β¬ π¦π πΆ β§ βπ¦ β π΄ (πΆπ π¦ β βπ§ β π΅ π§π π¦)) β inf(π΅, π΄, π ) = πΆ)) | ||
Theorem | eqinfd 9482* | Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 3-Sep-2020.) |
β’ (π β π Or π΄) & β’ (π β πΆ β π΄) & β’ ((π β§ π¦ β π΅) β Β¬ π¦π πΆ) & β’ ((π β§ (π¦ β π΄ β§ πΆπ π¦)) β βπ§ β π΅ π§π π¦) β β’ (π β inf(π΅, π΄, π ) = πΆ) | ||
Theorem | infval 9483* | Alternate expression for the infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π β π Or π΄) β β’ (π β inf(π΅, π΄, π ) = (β©π₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦)))) | ||
Theorem | infcllem 9484* | Lemma for infcl 9485, inflb 9486, infglb 9487, etc. (Contributed by AV, 3-Sep-2020.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯β‘π π¦ β§ βπ¦ β π΄ (π¦β‘π π₯ β βπ§ β π΅ π¦β‘π π§))) | ||
Theorem | infcl 9485* | An infimum belongs to its base class (closure law). See also inflb 9486 and infglb 9487. (Contributed by AV, 3-Sep-2020.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β inf(π΅, π΄, π ) β π΄) | ||
Theorem | inflb 9486* | An infimum is a lower bound. See also infcl 9485 and infglb 9487. (Contributed by AV, 3-Sep-2020.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β (πΆ β π΅ β Β¬ πΆπ inf(π΅, π΄, π ))) | ||
Theorem | infglb 9487* | An infimum is the greatest lower bound. See also infcl 9485 and inflb 9486. (Contributed by AV, 3-Sep-2020.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β ((πΆ β π΄ β§ inf(π΅, π΄, π )π πΆ) β βπ§ β π΅ π§π πΆ)) | ||
Theorem | infglbb 9488* | Bidirectional form of infglb 9487. (Contributed by AV, 3-Sep-2020.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) & β’ (π β π΅ β π΄) β β’ ((π β§ πΆ β π΄) β (inf(π΅, π΄, π )π πΆ β βπ§ β π΅ π§π πΆ)) | ||
Theorem | infnlb 9489* | A lower bound is not greater than the infimum. (Contributed by AV, 3-Sep-2020.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β ((πΆ β π΄ β§ βπ§ β π΅ Β¬ π§π πΆ) β Β¬ inf(π΅, π΄, π )π πΆ)) | ||
Theorem | infex 9490 | An infimum is a set. (Contributed by AV, 3-Sep-2020.) |
β’ π Or π΄ β β’ inf(π΅, π΄, π ) β V | ||
Theorem | infmin 9491* | The smallest element of a set is its infimum. Note that the converse is not true; the infimum might not be an element of the set considered. (Contributed by AV, 3-Sep-2020.) |
β’ (π β π Or π΄) & β’ (π β πΆ β π΄) & β’ (π β πΆ β π΅) & β’ ((π β§ π¦ β π΅) β Β¬ π¦π πΆ) β β’ (π β inf(π΅, π΄, π ) = πΆ) | ||
Theorem | infmo 9492* | Any class π΅ has at most one infimum in π΄ (where π is interpreted as 'less than'). (Contributed by AV, 6-Oct-2020.) |
β’ (π β π Or π΄) β β’ (π β β*π₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) | ||
Theorem | infeu 9493* | An infimum is unique. (Contributed by AV, 6-Oct-2020.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β β!π₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) | ||
Theorem | fimin2g 9494* | A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020.) |
β’ ((π Or π΄ β§ π΄ β Fin β§ π΄ β β ) β βπ₯ β π΄ βπ¦ β π΄ Β¬ π¦π π₯) | ||
Theorem | fiming 9495* | A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020.) |
β’ ((π Or π΄ β§ π΄ β Fin β§ π΄ β β ) β βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦ β π₯π π¦)) | ||
Theorem | fiinfg 9496* | Lemma showing existence and closure of infimum of a finite set. (Contributed by AV, 6-Oct-2020.) |
β’ ((π Or π΄ β§ π΄ β Fin β§ π΄ β β ) β βπ₯ β π΄ (βπ¦ β π΄ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΄ π§π π¦))) | ||
Theorem | fiinf2g 9497* | A finite set satisfies the conditions to have an infimum. (Contributed by AV, 6-Oct-2020.) |
β’ ((π Or π΄ β§ (π΅ β Fin β§ π΅ β β β§ π΅ β π΄)) β βπ₯ β π΅ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) | ||
Theorem | fiinfcl 9498 | A nonempty finite set contains its infimum. (Contributed by AV, 3-Sep-2020.) |
β’ ((π Or π΄ β§ (π΅ β Fin β§ π΅ β β β§ π΅ β π΄)) β inf(π΅, π΄, π ) β π΅) | ||
Theorem | infltoreq 9499 | The infimum of a finite set is less than or equal to all the elements of the set. (Contributed by AV, 4-Sep-2020.) |
β’ (π β π Or π΄) & β’ (π β π΅ β π΄) & β’ (π β π΅ β Fin) & β’ (π β πΆ β π΅) & β’ (π β π = inf(π΅, π΄, π )) β β’ (π β (ππ πΆ β¨ πΆ = π)) | ||
Theorem | infpr 9500 | The infimum of a pair. (Contributed by AV, 4-Sep-2020.) |
β’ ((π Or π΄ β§ π΅ β π΄ β§ πΆ β π΄) β inf({π΅, πΆ}, π΄, π ) = if(π΅π πΆ, π΅, πΆ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |