![]() |
Metamath
Proof Explorer Theorem List (p. 359 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ellines 35801* | Membership in the set of all lines. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (π΄ β LinesEE β βπ β β βπ β (πΌβπ)βπ β (πΌβπ)(π β π β§ π΄ = (πLineπ))) | ||
Theorem | linethru 35802 | If π΄ is a line containing two distinct points π and π, then π΄ is the line through π and π. Theorem 6.18 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π΄ β LinesEE β§ (π β π΄ β§ π β π΄) β§ π β π) β π΄ = (πLineπ)) | ||
Theorem | hilbert1.1 35803* | There is a line through any two distinct points. Hilbert's axiom I.1 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π)) β βπ₯ β LinesEE (π β π₯ β§ π β π₯)) | ||
Theorem | hilbert1.2 35804* | There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by NM, 17-Jun-2017.) |
β’ (π β π β β*π₯ β LinesEE (π β π₯ β§ π β π₯)) | ||
Theorem | linethrueu 35805* | There is a unique line going through any two distinct points. Theorem 6.19 of [Schwabhauser] p. 46. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π)) β β!π₯ β LinesEE (π β π₯ β§ π β π₯)) | ||
Theorem | lineintmo 35806* | Two distinct lines intersect in at most one point. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π΄ β LinesEE β§ π΅ β LinesEE β§ π΄ β π΅) β β*π₯(π₯ β π΄ β§ π₯ β π΅)) | ||
Syntax | cfwddif 35807 | Declare the syntax for the forward difference operator. |
class β³ | ||
Definition | df-fwddif 35808* | Define the forward difference operator. This is a discrete analogue of the derivative operator. Definition 2.42 of [GramKnuthPat], p. 47. (Contributed by Scott Fenton, 18-May-2020.) |
β’ β³ = (π β (β βpm β) β¦ (π₯ β {π¦ β dom π β£ (π¦ + 1) β dom π} β¦ ((πβ(π₯ + 1)) β (πβπ₯)))) | ||
Syntax | cfwddifn 35809 | Declare the syntax for the nth forward difference operator. |
class β³n | ||
Definition | df-fwddifn 35810* | Define the nth forward difference operator. This works out to be the forward difference operator iterated π times. (Contributed by Scott Fenton, 28-May-2020.) |
β’ β³n = (π β β0, π β (β βpm β) β¦ (π₯ β {π¦ β β β£ βπ β (0...π)(π¦ + π) β dom π} β¦ Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πβ(π₯ + π)))))) | ||
Theorem | fwddifval 35811 | Calculate the value of the forward difference operator at a point. (Contributed by Scott Fenton, 18-May-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π β π΄) & β’ (π β (π + 1) β π΄) β β’ (π β (( β³ βπΉ)βπ) = ((πΉβ(π + 1)) β (πΉβπ))) | ||
Theorem | fwddifnval 35812* | The value of the forward difference operator at a point. (Contributed by Scott Fenton, 28-May-2020.) |
β’ (π β π β β0) & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π β β) & β’ ((π β§ π β (0...π)) β (π + π) β π΄) β β’ (π β ((π β³n πΉ)βπ) = Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π))))) | ||
Theorem | fwddifn0 35813 | The value of the n-iterated forward difference operator at zero is just the function value. (Contributed by Scott Fenton, 28-May-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π β π΄) β β’ (π β ((0 β³n πΉ)βπ) = (πΉβπ)) | ||
Theorem | fwddifnp1 35814* | The value of the n-iterated forward difference at a successor. (Contributed by Scott Fenton, 28-May-2020.) |
β’ (π β π β β0) & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π β β) & β’ ((π β§ π β (0...(π + 1))) β (π + π) β π΄) β β’ (π β (((π + 1) β³n πΉ)βπ) = (((π β³n πΉ)β(π + 1)) β ((π β³n πΉ)βπ))) | ||
Theorem | rankung 35815 | The rank of the union of two sets. Closed form of rankun 9874. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ ((π΄ β π β§ π΅ β π) β (rankβ(π΄ βͺ π΅)) = ((rankβπ΄) βͺ (rankβπ΅))) | ||
Theorem | ranksng 35816 | The rank of a singleton. Closed form of ranksn 9872. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ (π΄ β π β (rankβ{π΄}) = suc (rankβπ΄)) | ||
Theorem | rankelg 35817 | The membership relation is inherited by the rank function. Closed form of rankel 9857. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ ((π΅ β π β§ π΄ β π΅) β (rankβπ΄) β (rankβπ΅)) | ||
Theorem | rankpwg 35818 | The rank of a power set. Closed form of rankpw 9861. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ (π΄ β π β (rankβπ« π΄) = suc (rankβπ΄)) | ||
Theorem | rank0 35819 | The rank of the empty set is β . (Contributed by Scott Fenton, 17-Jul-2015.) |
β’ (rankββ ) = β | ||
Theorem | rankeq1o 35820 | The only set with rank 1o is the singleton of the empty set. (Contributed by Scott Fenton, 17-Jul-2015.) |
β’ ((rankβπ΄) = 1o β π΄ = {β }) | ||
Syntax | chf 35821 | The constant Hf is a class. |
class Hf | ||
Definition | df-hf 35822 | Define the hereditarily finite sets. These are the finite sets whose elements are finite, and so forth. (Contributed by Scott Fenton, 9-Jul-2015.) |
β’ Hf = βͺ (π 1 β Ο) | ||
Theorem | elhf 35823* | Membership in the hereditarily finite sets. (Contributed by Scott Fenton, 9-Jul-2015.) |
β’ (π΄ β Hf β βπ₯ β Ο π΄ β (π 1βπ₯)) | ||
Theorem | elhf2 35824 | Alternate form of membership in the hereditarily finite sets. (Contributed by Scott Fenton, 13-Jul-2015.) |
β’ π΄ β V β β’ (π΄ β Hf β (rankβπ΄) β Ο) | ||
Theorem | elhf2g 35825 | Hereditarily finiteness via rank. Closed form of elhf2 35824. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ (π΄ β π β (π΄ β Hf β (rankβπ΄) β Ο)) | ||
Theorem | 0hf 35826 | The empty set is a hereditarily finite set. (Contributed by Scott Fenton, 9-Jul-2015.) |
β’ β β Hf | ||
Theorem | hfun 35827 | The union of two HF sets is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ ((π΄ β Hf β§ π΅ β Hf ) β (π΄ βͺ π΅) β Hf ) | ||
Theorem | hfsn 35828 | The singleton of an HF set is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ (π΄ β Hf β {π΄} β Hf ) | ||
Theorem | hfadj 35829 | Adjoining one HF element to an HF set preserves HF status. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ ((π΄ β Hf β§ π΅ β Hf ) β (π΄ βͺ {π΅}) β Hf ) | ||
Theorem | hfelhf 35830 | Any member of an HF set is itself an HF set. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ ((π΄ β π΅ β§ π΅ β Hf ) β π΄ β Hf ) | ||
Theorem | hftr 35831 | The class of all hereditarily finite sets is transitive. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ Tr Hf | ||
Theorem | hfext 35832* | Extensionality for HF sets depends only on comparison of HF elements. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ ((π΄ β Hf β§ π΅ β Hf ) β (π΄ = π΅ β βπ₯ β Hf (π₯ β π΄ β π₯ β π΅))) | ||
Theorem | hfuni 35833 | The union of an HF set is itself hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ (π΄ β Hf β βͺ π΄ β Hf ) | ||
Theorem | hfpw 35834 | The power class of an HF set is hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ (π΄ β Hf β π« π΄ β Hf ) | ||
Theorem | hfninf 35835 | Ο is not hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ Β¬ Ο β Hf | ||
Theorem | mpomulnzcnf 35836* | Multiplication maps nonzero complex numbers to nonzero complex numbers. Version of mulnzcnf 11885 using maps-to notation, which does not require ax-mulf 11213. (Contributed by GG, 18-Apr-2025.) |
β’ (π₯ β (β β {0}), π¦ β (β β {0}) β¦ (π₯ Β· π¦)):((β β {0}) Γ (β β {0}))βΆ(β β {0}) | ||
Theorem | a1i14 35837 | Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.) |
β’ (π β (π β π)) β β’ (π β (π β (π β (π β π)))) | ||
Theorem | a1i24 35838 | Add two antecedents to a wff. Deduction associated with a1i13 27. (Contributed by Jeff Hankins, 5-Aug-2009.) |
β’ (π β (π β π)) β β’ (π β (π β (π β (π β π)))) | ||
Theorem | exp5d 35839 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ (((π β§ π) β§ π) β ((π β§ π) β π)) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp5g 35840 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ π) β (((π β§ π) β§ π) β π)) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp5k 35841 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ (π β (((π β§ (π β§ π)) β§ π) β π)) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp56 35842 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((((π β§ π) β§ π) β§ (π β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp58 35843 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ (((π β§ π) β§ ((π β§ π) β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp510 35844 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ (((π β§ π) β§ π) β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp511 35845 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ ((π β§ (π β§ π)) β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp512 35846 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ ((π β§ π) β§ (π β§ π))) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | 3com12d 35847 | Commutation in consequent. Swap 1st and 2nd. (Contributed by Jeff Hankins, 17-Nov-2009.) |
β’ (π β (π β§ π β§ π)) β β’ (π β (π β§ π β§ π)) | ||
Theorem | imp5p 35848 | A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.) |
β’ (π β (π β (π β (π β (π β π))))) β β’ (π β (π β ((π β§ π β§ π) β π))) | ||
Theorem | imp5q 35849 | A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.) |
β’ (π β (π β (π β (π β (π β π))))) β β’ ((π β§ π) β ((π β§ π β§ π) β π)) | ||
Theorem | ecase13d 35850 | Deduction for elimination by cases. (Contributed by Jeff Hankins, 18-Aug-2009.) |
β’ (π β Β¬ π) & β’ (π β Β¬ π) & β’ (π β (π β¨ π β¨ π)) β β’ (π β π) | ||
Theorem | subtr 35851 | Transitivity of implicit substitution. (Contributed by Jeff Hankins, 13-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π & β’ β²π₯π & β’ (π₯ = π΄ β π = π) & β’ (π₯ = π΅ β π = π) β β’ ((π΄ β πΆ β§ π΅ β π·) β (π΄ = π΅ β π = π)) | ||
Theorem | subtr2 35852 | Transitivity of implicit substitution into a wff. (Contributed by Jeff Hankins, 19-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π & β’ β²π₯π & β’ (π₯ = π΄ β (π β π)) & β’ (π₯ = π΅ β (π β π)) β β’ ((π΄ β πΆ β§ π΅ β π·) β (π΄ = π΅ β (π β π))) | ||
Theorem | trer 35853* | A relation intersected with its converse is an equivalence relation if the relation is transitive. (Contributed by Jeff Hankins, 6-Oct-2009.) (Revised by Mario Carneiro, 12-Aug-2015.) |
β’ (βπβπβπ((π β€ π β§ π β€ π) β π β€ π) β ( β€ β© β‘ β€ ) Er dom ( β€ β© β‘ β€ )) | ||
Theorem | elicc3 35854 | An equivalent membership condition for closed intervals. (Contributed by Jeff Hankins, 14-Jul-2009.) |
β’ ((π΄ β β* β§ π΅ β β*) β (πΆ β (π΄[,]π΅) β (πΆ β β* β§ π΄ β€ π΅ β§ (πΆ = π΄ β¨ (π΄ < πΆ β§ πΆ < π΅) β¨ πΆ = π΅)))) | ||
Theorem | finminlem 35855* | A useful lemma about finite sets. If a property holds for a finite set, it holds for a minimal set. (Contributed by Jeff Hankins, 4-Dec-2009.) |
β’ (π₯ = π¦ β (π β π)) β β’ (βπ₯ β Fin π β βπ₯(π β§ βπ¦((π¦ β π₯ β§ π) β π₯ = π¦))) | ||
Theorem | gtinf 35856* | Any number greater than an infimum is greater than some element of the set. (Contributed by Jeff Hankins, 29-Sep-2013.) (Revised by AV, 10-Oct-2021.) |
β’ (((π β β β§ π β β β§ βπ₯ β β βπ¦ β π π₯ β€ π¦) β§ (π΄ β β β§ inf(π, β, < ) < π΄)) β βπ§ β π π§ < π΄) | ||
Theorem | opnrebl 35857* | A set is open in the standard topology of the reals precisely when every point can be enclosed in an open ball. (Contributed by Jeff Hankins, 23-Sep-2013.) (Proof shortened by Mario Carneiro, 30-Jan-2014.) |
β’ (π΄ β (topGenβran (,)) β (π΄ β β β§ βπ₯ β π΄ βπ¦ β β+ ((π₯ β π¦)(,)(π₯ + π¦)) β π΄)) | ||
Theorem | opnrebl2 35858* | A set is open in the standard topology of the reals precisely when every point can be enclosed in an arbitrarily small ball. (Contributed by Jeff Hankins, 22-Sep-2013.) (Proof shortened by Mario Carneiro, 30-Jan-2014.) |
β’ (π΄ β (topGenβran (,)) β (π΄ β β β§ βπ₯ β π΄ βπ¦ β β+ βπ§ β β+ (π§ β€ π¦ β§ ((π₯ β π§)(,)(π₯ + π§)) β π΄))) | ||
Theorem | nn0prpwlem 35859* | Lemma for nn0prpw 35860. Use strong induction to show that every positive integer has unique prime power divisors. (Contributed by Jeff Hankins, 28-Sep-2013.) |
β’ (π΄ β β β βπ β β (π < π΄ β βπ β β βπ β β Β¬ ((πβπ) β₯ π β (πβπ) β₯ π΄))) | ||
Theorem | nn0prpw 35860* | Two nonnegative integers are the same if and only if they are divisible by the same prime powers. (Contributed by Jeff Hankins, 29-Sep-2013.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ = π΅ β βπ β β βπ β β ((πβπ) β₯ π΄ β (πβπ) β₯ π΅))) | ||
Theorem | topbnd 35861 | Two equivalent expressions for the boundary of a topology. (Contributed by Jeff Hankins, 23-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄))) = (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) | ||
Theorem | opnbnd 35862 | A set is open iff it is disjoint from its boundary. (Contributed by Jeff Hankins, 23-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (π΄ β π½ β (π΄ β© (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄)))) = β )) | ||
Theorem | cldbnd 35863 | A set is closed iff it contains its boundary. (Contributed by Jeff Hankins, 1-Oct-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (π΄ β (Clsdβπ½) β (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄))) β π΄)) | ||
Theorem | ntruni 35864* | A union of interiors is a subset of the interior of the union. The reverse inclusion may not hold. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π« π) β βͺ π β π ((intβπ½)βπ) β ((intβπ½)ββͺ π)) | ||
Theorem | clsun 35865 | A pairwise union of closures is the closure of the union. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((clsβπ½)β(π΄ βͺ π΅)) = (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅))) | ||
Theorem | clsint2 35866* | The closure of an intersection is a subset of the intersection of the closures. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ πΆ β π« π) β ((clsβπ½)ββ© πΆ) β β© π β πΆ ((clsβπ½)βπ)) | ||
Theorem | opnregcld 35867* | A set is regularly closed iff it is the closure of some open set. (Contributed by Jeff Hankins, 27-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (((clsβπ½)β((intβπ½)βπ΄)) = π΄ β βπ β π½ π΄ = ((clsβπ½)βπ))) | ||
Theorem | cldregopn 35868* | A set if regularly open iff it is the interior of some closed set. (Contributed by Jeff Hankins, 27-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (((intβπ½)β((clsβπ½)βπ΄)) = π΄ β βπ β (Clsdβπ½)π΄ = ((intβπ½)βπ))) | ||
Theorem | neiin 35869 | Two neighborhoods intersect to form a neighborhood of the intersection. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄) β§ π β ((neiβπ½)βπ΅)) β (π β© π) β ((neiβπ½)β(π΄ β© π΅))) | ||
Theorem | hmeoclda 35870 | Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.) (Revised by Mario Carneiro, 3-Jun-2014.) |
β’ (((π½ β Top β§ πΎ β Top β§ πΉ β (π½HomeoπΎ)) β§ π β (Clsdβπ½)) β (πΉ β π) β (ClsdβπΎ)) | ||
Theorem | hmeocldb 35871 | Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.) |
β’ (((π½ β Top β§ πΎ β Top β§ πΉ β (π½HomeoπΎ)) β§ π β (ClsdβπΎ)) β (β‘πΉ β π) β (Clsdβπ½)) | ||
Theorem | ivthALT 35872* | An alternate proof of the Intermediate Value Theorem ivth 25396 using topology. (Contributed by Jeff Hankins, 17-Aug-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (((π΄ β β β§ π΅ β β β§ π β β) β§ π΄ < π΅ β§ ((π΄[,]π΅) β π· β§ π· β β β§ (πΉ β (π·βcnββ) β§ (πΉ β (π΄[,]π΅)) β β β§ π β ((πΉβπ΄)(,)(πΉβπ΅))))) β βπ₯ β (π΄(,)π΅)(πΉβπ₯) = π) | ||
Syntax | cfne 35873 | Extend class definition to include the "finer than" relation. |
class Fne | ||
Definition | df-fne 35874* | Define the fineness relation for covers. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ Fne = {β¨π₯, π¦β© β£ (βͺ π₯ = βͺ π¦ β§ βπ§ β π₯ π§ β βͺ (π¦ β© π« π§))} | ||
Theorem | fnerel 35875 | Fineness is a relation. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ Rel Fne | ||
Theorem | isfne 35876* | The predicate "π΅ is finer than π΄". This property is, in a sense, the opposite of refinement, as refinement requires every element to be a subset of an element of the original and fineness requires that every element of the original have a subset in the finer cover containing every point. I do not know of a literature reference for this. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΅ β πΆ β (π΄Fneπ΅ β (π = π β§ βπ₯ β π΄ π₯ β βͺ (π΅ β© π« π₯)))) | ||
Theorem | isfne4 35877 | The predicate "π΅ is finer than π΄ " in terms of the topology generation function. (Contributed by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΄Fneπ΅ β (π = π β§ π΄ β (topGenβπ΅))) | ||
Theorem | isfne4b 35878 | A condition for a topology to be finer than another. (Contributed by Jeff Hankins, 28-Sep-2009.) (Revised by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΅ β π β (π΄Fneπ΅ β (π = π β§ (topGenβπ΄) β (topGenβπ΅)))) | ||
Theorem | isfne2 35879* | The predicate "π΅ is finer than π΄". (Contributed by Jeff Hankins, 28-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΅ β πΆ β (π΄Fneπ΅ β (π = π β§ βπ₯ β π΄ βπ¦ β π₯ βπ§ β π΅ (π¦ β π§ β§ π§ β π₯)))) | ||
Theorem | isfne3 35880* | The predicate "π΅ is finer than π΄". (Contributed by Jeff Hankins, 11-Oct-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΅ β πΆ β (π΄Fneπ΅ β (π = π β§ βπ₯ β π΄ βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦)))) | ||
Theorem | fnebas 35881 | A finer cover covers the same set as the original. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΄Fneπ΅ β π = π) | ||
Theorem | fnetg 35882 | A finer cover generates a topology finer than the original set. (Contributed by Mario Carneiro, 11-Sep-2015.) |
β’ (π΄Fneπ΅ β π΄ β (topGenβπ΅)) | ||
Theorem | fnessex 35883* | If π΅ is finer than π΄ and π is an element of π΄, every point in π is an element of a subset of π which is in π΅. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ ((π΄Fneπ΅ β§ π β π΄ β§ π β π) β βπ₯ β π΅ (π β π₯ β§ π₯ β π)) | ||
Theorem | fneuni 35884* | If π΅ is finer than π΄, every element of π΄ is a union of elements of π΅. (Contributed by Jeff Hankins, 11-Oct-2009.) |
β’ ((π΄Fneπ΅ β§ π β π΄) β βπ₯(π₯ β π΅ β§ π = βͺ π₯)) | ||
Theorem | fneint 35885* | If a cover is finer than another, every point can be approached more closely by intersections. (Contributed by Jeff Hankins, 11-Oct-2009.) |
β’ (π΄Fneπ΅ β β© {π₯ β π΅ β£ π β π₯} β β© {π₯ β π΄ β£ π β π₯}) | ||
Theorem | fness 35886 | A cover is finer than its subcovers. (Contributed by Jeff Hankins, 11-Oct-2009.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ ((π΅ β πΆ β§ π΄ β π΅ β§ π = π) β π΄Fneπ΅) | ||
Theorem | fneref 35887 | Reflexivity of the fineness relation. (Contributed by Jeff Hankins, 12-Oct-2009.) |
β’ (π΄ β π β π΄Fneπ΄) | ||
Theorem | fnetr 35888 | Transitivity of the fineness relation. (Contributed by Jeff Hankins, 5-Oct-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ ((π΄Fneπ΅ β§ π΅FneπΆ) β π΄FneπΆ) | ||
Theorem | fneval 35889 | Two covers are finer than each other iff they are both bases for the same topology. (Contributed by Mario Carneiro, 11-Sep-2015.) |
β’ βΌ = (Fne β© β‘Fne) β β’ ((π΄ β π β§ π΅ β π) β (π΄ βΌ π΅ β (topGenβπ΄) = (topGenβπ΅))) | ||
Theorem | fneer 35890 | Fineness intersected with its converse is an equivalence relation. (Contributed by Jeff Hankins, 6-Oct-2009.) (Revised by Mario Carneiro, 11-Sep-2015.) |
β’ βΌ = (Fne β© β‘Fne) β β’ βΌ Er V | ||
Theorem | topfne 35891 | Fineness for covers corresponds precisely with fineness for topologies. (Contributed by Jeff Hankins, 29-Sep-2009.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ ((πΎ β Top β§ π = π) β (π½ β πΎ β π½FneπΎ)) | ||
Theorem | topfneec 35892 | A cover is equivalent to a topology iff it is a base for that topology. (Contributed by Jeff Hankins, 8-Oct-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ βΌ = (Fne β© β‘Fne) β β’ (π½ β Top β (π΄ β [π½] βΌ β (topGenβπ΄) = π½)) | ||
Theorem | topfneec2 35893 | A topology is precisely identified with its equivalence class. (Contributed by Jeff Hankins, 12-Oct-2009.) |
β’ βΌ = (Fne β© β‘Fne) β β’ ((π½ β Top β§ πΎ β Top) β ([π½] βΌ = [πΎ] βΌ β π½ = πΎ)) | ||
Theorem | fnessref 35894* | A cover is finer iff it has a subcover which is both finer and a refinement. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π = π β (π΄Fneπ΅ β βπ(π β π΅ β§ (π΄Fneπ β§ πRefπ΄)))) | ||
Theorem | refssfne 35895* | A cover is a refinement iff it is a subcover of something which is both finer and a refinement. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π = π β (π΅Refπ΄ β βπ(π΅ β π β§ (π΄Fneπ β§ πRefπ΄)))) | ||
Theorem | neibastop1 35896* | A collection of neighborhood bases determines a topology. Part of Theorem 4.5 of Stephen Willard's General Topology. (Contributed by Jeff Hankins, 8-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(π« π« π β {β })) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯) β§ π€ β (πΉβπ₯))) β ((πΉβπ₯) β© π« (π£ β© π€)) β β ) & β’ π½ = {π β π« π β£ βπ₯ β π ((πΉβπ₯) β© π« π) β β } β β’ (π β π½ β (TopOnβπ)) | ||
Theorem | neibastop2lem 35897* | Lemma for neibastop2 35898. (Contributed by Jeff Hankins, 12-Sep-2009.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(π« π« π β {β })) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯) β§ π€ β (πΉβπ₯))) β ((πΉβπ₯) β© π« (π£ β© π€)) β β ) & β’ π½ = {π β π« π β£ βπ₯ β π ((πΉβπ₯) β© π« π) β β } & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β π₯ β π£) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β βπ‘ β (πΉβπ₯)βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (πΉβπ)) & β’ (π β π β π) & β’ πΊ = (rec((π β V β¦ βͺ π§ β π βͺ π₯ β π ((πΉβπ₯) β© π« π§)), {π}) βΎ Ο) & β’ π = {π¦ β π β£ βπ β βͺ ran πΊ((πΉβπ¦) β© π« π) β β } β β’ (π β βπ’ β π½ (π β π’ β§ π’ β π)) | ||
Theorem | neibastop2 35898* | In the topology generated by a neighborhood base, a set is a neighborhood of a point iff it contains a subset in the base. (Contributed by Jeff Hankins, 9-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(π« π« π β {β })) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯) β§ π€ β (πΉβπ₯))) β ((πΉβπ₯) β© π« (π£ β© π€)) β β ) & β’ π½ = {π β π« π β£ βπ₯ β π ((πΉβπ₯) β© π« π) β β } & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β π₯ β π£) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β βπ‘ β (πΉβπ₯)βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β ) β β’ ((π β§ π β π) β (π β ((neiβπ½)β{π}) β (π β π β§ ((πΉβπ) β© π« π) β β ))) | ||
Theorem | neibastop3 35899* | The topology generated by a neighborhood base is unique. (Contributed by Jeff Hankins, 16-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ (π β π β π) & β’ (π β πΉ:πβΆ(π« π« π β {β })) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯) β§ π€ β (πΉβπ₯))) β ((πΉβπ₯) β© π« (π£ β© π€)) β β ) & β’ π½ = {π β π« π β£ βπ₯ β π ((πΉβπ₯) β© π« π) β β } & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β π₯ β π£) & β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β βπ‘ β (πΉβπ₯)βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β ) β β’ (π β β!π β (TopOnβπ)βπ₯ β π ((neiβπ)β{π₯}) = {π β π« π β£ ((πΉβπ₯) β© π« π) β β }) | ||
Theorem | topmtcl 35900 | The meet of a collection of topologies on π is again a topology on π. (Contributed by Jeff Hankins, 5-Oct-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ ((π β π β§ π β (TopOnβπ)) β (π« π β© β© π) β (TopOnβπ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |