![]() |
Metamath
Proof Explorer Theorem List (p. 95 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mapfienlem2 9401* | Lemma 2 for mapfien 9403. (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 9402* | Lemma 3 for mapfien 9403. (Contributed by AV, 3-Jul-2019.) (Revised by AV, 28-Jul-2024.) |
β’ π = {π₯ β (π΅ βm π΄) β£ π₯ finSupp π} & β’ π = {π₯ β (π· βm πΆ) β£ π₯ finSupp π} & β’ π = (πΊβπ) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄) & β’ (π β πΊ:π΅β1-1-ontoβπ·) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) & β’ (π β π β π΅) β β’ ((π β§ π β π) β ((β‘πΊ β π) β β‘πΉ) β π) | ||
Theorem | mapfien 9403* | 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 9404* | 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 9405 | 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 9406* | 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 9409). (Contributed by FL, 27-Apr-2008.) |
β’ fi = (π₯ β V β¦ {π§ β£ βπ¦ β (π« π₯ β© Fin)π§ = β© π¦}) | ||
Theorem | fival 9407* | 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 9408* | Specific properties of an element of (fiβπ΅). (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄ β (fiβπ΅) β βπ₯ β (π« π΅ β© Fin)π΄ = β© π₯)) | ||
Theorem | elfi2 9409* | The empty intersection need not be considered in the set of finite intersections. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ (π΅ β π β (π΄ β (fiβπ΅) β βπ₯ β ((π« π΅ β© Fin) β {β })π΄ = β© π₯)) | ||
Theorem | elfir 9410 | Sufficient condition for an element of (fiβπ΅). (Contributed by Mario Carneiro, 24-Nov-2013.) |
β’ ((π΅ β π β§ (π΄ β π΅ β§ π΄ β β β§ π΄ β Fin)) β β© π΄ β (fiβπ΅)) | ||
Theorem | intrnfi 9411 | 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 9412* | 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 9413 | The intersection of two sets is a finite intersection. (Contributed by Thierry Arnoux, 6-Jan-2017.) |
β’ ((π β π β§ π΄ β π β§ π΅ β π) β (π΄ β© π΅) β (fiβπ)) | ||
Theorem | ssfii 9414 | 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 9415 | The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.) |
β’ (fiββ ) = β | ||
Theorem | fieq0 9416 | 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 9417 | The elements of (fiβπΆ) are closed under finite intersection. (Contributed by Mario Carneiro, 24-Nov-2013.) |
β’ ((π΄ β (fiβπΆ) β§ π΅ β (fiβπΆ)) β (π΄ β© π΅) β (fiβπΆ)) | ||
Theorem | dffi2 9418* | 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 9419 | Subset relationship for function fi. (Contributed by Jeff Hankins, 7-Oct-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
β’ ((π΅ β π β§ π΄ β π΅) β (fiβπ΄) β (fiβπ΅)) | ||
Theorem | inficl 9420* | 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 9421 | 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 9422 | A singleton is closed under finite intersections. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (fiβ{π΄}) = {π΄} | ||
Theorem | fiuni 9423 | 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 9424 | 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 9425* | 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 9426* | 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 9427* | Describe a surjection from nonempty finite sets to finite intersections. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ πΉ = (π¦ β ((π« π΄ β© Fin) β {β }) β¦ β© π¦) β β’ (π΄ β π β πΉ:((π« π΄ β© Fin) β {β })βontoβ(fiβπ΄)) | ||
Theorem | marypha1lem 9428* | Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015.) |
β’ (π΄ β Fin β (π β Fin β βπ β π« (π΄ Γ π)(βπ β π« π΄π βΌ (π β π) β βπ β π« ππ:π΄β1-1βV))) | ||
Theorem | marypha1 9429* | (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 9430* | Lemma for marypha2 9434. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
β’ π = βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β β’ π β (π΄ Γ βͺ ran πΉ) | ||
Theorem | marypha2lem2 9431* | Lemma for marypha2 9434. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
β’ π = βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β β’ π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πΉβπ₯))} | ||
Theorem | marypha2lem3 9432* | Lemma for marypha2 9434. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
β’ π = βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β β’ ((πΉ Fn π΄ β§ πΊ Fn π΄) β (πΊ β π β βπ₯ β π΄ (πΊβπ₯) β (πΉβπ₯))) | ||
Theorem | marypha2lem4 9433* | Lemma for marypha2 9434. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
β’ π = βͺ π₯ β π΄ ({π₯} Γ (πΉβπ₯)) β β’ ((πΉ Fn π΄ β§ π β π΄) β (π β π) = βͺ (πΉ β π)) | ||
Theorem | marypha2 9434* | Version of marypha1 9429 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 9435 | 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 9436 | 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 9437* | 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 15184. See dfsup2 9439 for alternate definition not requiring dummy variables. (Contributed by NM, 22-May-1999.) |
β’ sup(π΄, π΅, π ) = βͺ {π₯ β π΅ β£ (βπ¦ β π΄ Β¬ π₯π π¦ β§ βπ¦ β π΅ (π¦π π₯ β βπ§ β π΄ π¦π π§))} | ||
Definition | df-inf 9438 | 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 9439 | Quantifier-free definition of supremum. (Contributed by Scott Fenton, 19-Feb-2013.) |
β’ sup(π΅, π΄, π ) = βͺ (π΄ β ((β‘π β π΅) βͺ (π β (π΄ β (β‘π β π΅))))) | ||
Theorem | supeq1 9440 | Equality theorem for supremum. (Contributed by NM, 22-May-1999.) |
β’ (π΅ = πΆ β sup(π΅, π΄, π ) = sup(πΆ, π΄, π )) | ||
Theorem | supeq1d 9441 | Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ (π β π΅ = πΆ) β β’ (π β sup(π΅, π΄, π ) = sup(πΆ, π΄, π )) | ||
Theorem | supeq1i 9442 | Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ π΅ = πΆ β β’ sup(π΅, π΄, π ) = sup(πΆ, π΄, π ) | ||
Theorem | supeq2 9443 | Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π΅ = πΆ β sup(π΄, π΅, π ) = sup(π΄, πΆ, π )) | ||
Theorem | supeq3 9444 | Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.) |
β’ (π = π β sup(π΄, π΅, π ) = sup(π΄, π΅, π)) | ||
Theorem | supeq123d 9445 | Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
β’ (π β π΄ = π·) & β’ (π β π΅ = πΈ) & β’ (π β πΆ = πΉ) β β’ (π β sup(π΄, π΅, πΆ) = sup(π·, πΈ, πΉ)) | ||
Theorem | nfsup 9446 | Hypothesis builder for supremum. (Contributed by Mario Carneiro, 20-Mar-2014.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π β β’ β²π₯sup(π΄, π΅, π ) | ||
Theorem | supmo 9447* | 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 9448 | A supremum is a set. (Contributed by NM, 22-May-1999.) (Revised by Mario Carneiro, 24-Dec-2016.) |
β’ (π β π Or π΄) β β’ (π β sup(π΅, π΄, π ) β V) | ||
Theorem | supeu 9449* | 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 9450* | Alternate expression for the supremum. (Contributed by Mario Carneiro, 24-Dec-2016.) (Revised by Thierry Arnoux, 24-Sep-2017.) |
β’ (π β π Or π΄) β β’ (π β sup(π΅, π΄, π ) = (β©π₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§)))) | ||
Theorem | eqsup 9451* | Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015.) |
β’ (π β π Or π΄) β β’ (π β ((πΆ β π΄ β§ βπ¦ β π΅ Β¬ πΆπ π¦ β§ βπ¦ β π΄ (π¦π πΆ β βπ§ β π΅ π¦π π§)) β sup(π΅, π΄, π ) = πΆ)) | ||
Theorem | eqsupd 9452* | Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015.) |
β’ (π β π Or π΄) & β’ (π β πΆ β π΄) & β’ ((π β§ π¦ β π΅) β Β¬ πΆπ π¦) & β’ ((π β§ (π¦ β π΄ β§ π¦π πΆ)) β βπ§ β π΅ π¦π π§) β β’ (π β sup(π΅, π΄, π ) = πΆ) | ||
Theorem | supcl 9453* | A supremum belongs to its base class (closure law). See also supub 9454 and suplub 9455. (Contributed by NM, 12-Oct-2004.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β sup(π΅, π΄, π ) β π΄) | ||
Theorem | supub 9454* |
A supremum is an upper bound. See also supcl 9453 and suplub 9455.
This proof demonstrates how to expand an iota-based definition (df-iota 6496) using riotacl2 7382. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β (πΆ β π΅ β Β¬ sup(π΅, π΄, π )π πΆ)) | ||
Theorem | suplub 9455* | A supremum is the least upper bound. See also supcl 9453 and supub 9454. (Contributed by NM, 13-Oct-2004.) (Revised by Mario Carneiro, 24-Dec-2016.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β ((πΆ β π΄ β§ πΆπ sup(π΅, π΄, π )) β βπ§ β π΅ πΆπ π§)) | ||
Theorem | suplub2 9456* | Bidirectional form of suplub 9455. (Contributed by Mario Carneiro, 6-Sep-2014.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) & β’ (π β π΅ β π΄) β β’ ((π β§ πΆ β π΄) β (πΆπ sup(π΅, π΄, π ) β βπ§ β π΅ πΆπ π§)) | ||
Theorem | supnub 9457* | An upper bound is not less than the supremum. (Contributed by NM, 13-Oct-2004.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β ((πΆ β π΄ β§ βπ§ β π΅ Β¬ πΆπ π§) β Β¬ πΆπ sup(π΅, π΄, π ))) | ||
Theorem | supex 9458 | A supremum is a set. (Contributed by NM, 22-May-1999.) |
β’ π Or π΄ β β’ sup(π΅, π΄, π ) β V | ||
Theorem | sup00 9459 | The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
β’ sup(π΅, β , π ) = β | ||
Theorem | sup0riota 9460* | The supremum of an empty set is the smallest element of the base set. (Contributed by AV, 4-Sep-2020.) |
β’ (π Or π΄ β sup(β , π΄, π ) = (β©π₯ β π΄ βπ¦ β π΄ Β¬ π¦π π₯)) | ||
Theorem | sup0 9461* | 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 9462* | 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 9463* | A finite set satisfies the conditions to have a supremum. (Contributed by Mario Carneiro, 28-Apr-2015.) |
β’ ((π Or π΄ β§ (π΅ β Fin β§ π΅ β β β§ π΅ β π΄)) β βπ₯ β π΅ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) | ||
Theorem | fisupcl 9464 | A nonempty finite set contains its supremum. (Contributed by Jeff Madsen, 9-May-2011.) |
β’ ((π Or π΄ β§ (π΅ β Fin β§ π΅ β β β§ π΅ β π΄)) β sup(π΅, π΄, π ) β π΅) | ||
Theorem | supgtoreq 9465 | 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 9466 | The supremum of a pair. (Contributed by NM, 17-Jun-2007.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
β’ ((π Or π΄ β§ π΅ β π΄ β§ πΆ β π΄) β sup({π΅, πΆ}, π΄, π ) = if(πΆπ π΅, π΅, πΆ)) | ||
Theorem | supsn 9467 | The supremum of a singleton. (Contributed by NM, 2-Oct-2007.) |
β’ ((π Or π΄ β§ π΅ β π΄) β sup({π΅}, π΄, π ) = π΅) | ||
Theorem | supisolem 9468* | Lemma for supiso 9470. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ (π β πΉ Isom π , π (π΄, π΅)) & β’ (π β πΆ β π΄) β β’ ((π β§ π· β π΄) β ((βπ¦ β πΆ Β¬ π·π π¦ β§ βπ¦ β π΄ (π¦π π· β βπ§ β πΆ π¦π π§)) β (βπ€ β (πΉ β πΆ) Β¬ (πΉβπ·)ππ€ β§ βπ€ β π΅ (π€π(πΉβπ·) β βπ£ β (πΉ β πΆ)π€ππ£)))) | ||
Theorem | supisoex 9469* | Lemma for supiso 9470. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ (π β πΉ Isom π , π (π΄, π΅)) & β’ (π β πΆ β π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β πΆ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β πΆ π¦π π§))) β β’ (π β βπ’ β π΅ (βπ€ β (πΉ β πΆ) Β¬ π’ππ€ β§ βπ€ β π΅ (π€ππ’ β βπ£ β (πΉ β πΆ)π€ππ£))) | ||
Theorem | supiso 9470* | Image of a supremum under an isomorphism. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ (π β πΉ Isom π , π (π΄, π΅)) & β’ (π β πΆ β π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β πΆ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β πΆ π¦π π§))) & β’ (π β π Or π΄) β β’ (π β sup((πΉ β πΆ), π΅, π) = (πΉβsup(πΆ, π΄, π ))) | ||
Theorem | infeq1 9471 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π΅ = πΆ β inf(π΅, π΄, π ) = inf(πΆ, π΄, π )) | ||
Theorem | infeq1d 9472 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π β π΅ = πΆ) β β’ (π β inf(π΅, π΄, π ) = inf(πΆ, π΄, π )) | ||
Theorem | infeq1i 9473 | Equality inference for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ π΅ = πΆ β β’ inf(π΅, π΄, π ) = inf(πΆ, π΄, π ) | ||
Theorem | infeq2 9474 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π΅ = πΆ β inf(π΄, π΅, π ) = inf(π΄, πΆ, π )) | ||
Theorem | infeq3 9475 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π = π β inf(π΄, π΅, π ) = inf(π΄, π΅, π)) | ||
Theorem | infeq123d 9476 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π β π΄ = π·) & β’ (π β π΅ = πΈ) & β’ (π β πΆ = πΉ) β β’ (π β inf(π΄, π΅, πΆ) = inf(π·, πΈ, πΉ)) | ||
Theorem | nfinf 9477 | Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π β β’ β²π₯inf(π΄, π΅, π ) | ||
Theorem | infexd 9478 | An infimum is a set. (Contributed by AV, 2-Sep-2020.) |
β’ (π β π Or π΄) β β’ (π β inf(π΅, π΄, π ) β V) | ||
Theorem | eqinf 9479* | Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π β π Or π΄) β β’ (π β ((πΆ β π΄ β§ βπ¦ β π΅ Β¬ π¦π πΆ β§ βπ¦ β π΄ (πΆπ π¦ β βπ§ β π΅ π§π π¦)) β inf(π΅, π΄, π ) = πΆ)) | ||
Theorem | eqinfd 9480* | Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 3-Sep-2020.) |
β’ (π β π Or π΄) & β’ (π β πΆ β π΄) & β’ ((π β§ π¦ β π΅) β Β¬ π¦π πΆ) & β’ ((π β§ (π¦ β π΄ β§ πΆπ π¦)) β βπ§ β π΅ π§π π¦) β β’ (π β inf(π΅, π΄, π ) = πΆ) | ||
Theorem | infval 9481* | Alternate expression for the infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π β π Or π΄) β β’ (π β inf(π΅, π΄, π ) = (β©π₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦)))) | ||
Theorem | infcllem 9482* | Lemma for infcl 9483, inflb 9484, infglb 9485, etc. (Contributed by AV, 3-Sep-2020.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯β‘π π¦ β§ βπ¦ β π΄ (π¦β‘π π₯ β βπ§ β π΅ π¦β‘π π§))) | ||
Theorem | infcl 9483* | An infimum belongs to its base class (closure law). See also inflb 9484 and infglb 9485. (Contributed by AV, 3-Sep-2020.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β inf(π΅, π΄, π ) β π΄) | ||
Theorem | inflb 9484* | An infimum is a lower bound. See also infcl 9483 and infglb 9485. (Contributed by AV, 3-Sep-2020.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β (πΆ β π΅ β Β¬ πΆπ inf(π΅, π΄, π ))) | ||
Theorem | infglb 9485* | An infimum is the greatest lower bound. See also infcl 9483 and inflb 9484. (Contributed by AV, 3-Sep-2020.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β ((πΆ β π΄ β§ inf(π΅, π΄, π )π πΆ) β βπ§ β π΅ π§π πΆ)) | ||
Theorem | infglbb 9486* | Bidirectional form of infglb 9485. (Contributed by AV, 3-Sep-2020.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) & β’ (π β π΅ β π΄) β β’ ((π β§ πΆ β π΄) β (inf(π΅, π΄, π )π πΆ β βπ§ β π΅ π§π πΆ)) | ||
Theorem | infnlb 9487* | A lower bound is not greater than the infimum. (Contributed by AV, 3-Sep-2020.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β ((πΆ β π΄ β§ βπ§ β π΅ Β¬ π§π πΆ) β Β¬ inf(π΅, π΄, π )π πΆ)) | ||
Theorem | infex 9488 | An infimum is a set. (Contributed by AV, 3-Sep-2020.) |
β’ π Or π΄ β β’ inf(π΅, π΄, π ) β V | ||
Theorem | infmin 9489* | 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 9490* | Any class π΅ has at most one infimum in π΄ (where π is interpreted as 'less than'). (Contributed by AV, 6-Oct-2020.) |
β’ (π β π Or π΄) β β’ (π β β*π₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) | ||
Theorem | infeu 9491* | An infimum is unique. (Contributed by AV, 6-Oct-2020.) |
β’ (π β π Or π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β β!π₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) | ||
Theorem | fimin2g 9492* | A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020.) |
β’ ((π Or π΄ β§ π΄ β Fin β§ π΄ β β ) β βπ₯ β π΄ βπ¦ β π΄ Β¬ π¦π π₯) | ||
Theorem | fiming 9493* | A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020.) |
β’ ((π Or π΄ β§ π΄ β Fin β§ π΄ β β ) β βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦ β π₯π π¦)) | ||
Theorem | fiinfg 9494* | Lemma showing existence and closure of infimum of a finite set. (Contributed by AV, 6-Oct-2020.) |
β’ ((π Or π΄ β§ π΄ β Fin β§ π΄ β β ) β βπ₯ β π΄ (βπ¦ β π΄ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΄ π§π π¦))) | ||
Theorem | fiinf2g 9495* | A finite set satisfies the conditions to have an infimum. (Contributed by AV, 6-Oct-2020.) |
β’ ((π Or π΄ β§ (π΅ β Fin β§ π΅ β β β§ π΅ β π΄)) β βπ₯ β π΅ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) | ||
Theorem | fiinfcl 9496 | A nonempty finite set contains its infimum. (Contributed by AV, 3-Sep-2020.) |
β’ ((π Or π΄ β§ (π΅ β Fin β§ π΅ β β β§ π΅ β π΄)) β inf(π΅, π΄, π ) β π΅) | ||
Theorem | infltoreq 9497 | 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 9498 | The infimum of a pair. (Contributed by AV, 4-Sep-2020.) |
β’ ((π Or π΄ β§ π΅ β π΄ β§ πΆ β π΄) β inf({π΅, πΆ}, π΄, π ) = if(π΅π πΆ, π΅, πΆ)) | ||
Theorem | infsupprpr 9499 | The infimum of a proper pair is less than the supremum of this pair. (Contributed by AV, 13-Mar-2023.) |
β’ ((π Or π΄ β§ (π΅ β π΄ β§ πΆ β π΄ β§ π΅ β πΆ)) β inf({π΅, πΆ}, π΄, π )π sup({π΅, πΆ}, π΄, π )) | ||
Theorem | infsn 9500 | The infimum of a singleton. (Contributed by NM, 2-Oct-2007.) |
β’ ((π Or π΄ β§ π΅ β π΄) β inf({π΅}, π΄, π ) = π΅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |