Home | Metamath
Proof Explorer Theorem List (p. 347 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | outsideofeq 34601 | Uniqueness law for OutsideOf. Analogue of segconeq 34481. (Contributed by Scott Fenton, 24-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (((π΄OutsideOfβ¨π, π β© β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ (π΄OutsideOfβ¨π, π β© β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©)) β π = π)) | ||
Theorem | outsideofeu 34602* | Given a nondegenerate ray, there is a unique point congruent to the segment π΅πΆ lying on the ray π΄π . Theorem 6.11 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 23-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ πΆ β (πΌβπ))) β ((π β π΄ β§ π΅ β πΆ) β β!π₯ β (πΌβπ)(π΄OutsideOfβ¨π₯, π β© β§ β¨π΄, π₯β©Cgrβ¨π΅, πΆβ©))) | ||
Theorem | outsidele 34603 | Relate OutsideOf to Segβ€. Theorem 6.13 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 24-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β (β¨π, π΄β© Segβ€ β¨π, π΅β© β π΄ Btwn β¨π, π΅β©))) | ||
Theorem | outsideofcol 34604 | Outside of implies colinearity. (Contributed by Scott Fenton, 26-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (πOutsideOfβ¨π, π β© β π Colinear β¨π, π β©) | ||
Syntax | cline2 34605 | Declare the constant for the line function. |
class Line | ||
Syntax | cray 34606 | Declare the constant for the ray function. |
class Ray | ||
Syntax | clines2 34607 | Declare the constant for the set of all lines. |
class LinesEE | ||
Definition | df-line2 34608* | Define the Line function. This function generates the line passing through the distinct points π and π. Adapted from definition 6.14 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 25-Oct-2013.) |
β’ Line = {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )} | ||
Definition | df-ray 34609* | Define the Ray function. This function generates the set of all points that lie on the ray starting at π and passing through π. Definition 6.8 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 21-Oct-2013.) |
β’ Ray = {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©})} | ||
Definition | df-lines2 34610 | Define the set of all lines. Definition 6.14, part 2 of [Schwabhauser] p. 45. See ellines 34623 for membership. (Contributed by Scott Fenton, 28-Oct-2013.) |
β’ LinesEE = ran Line | ||
Theorem | funray 34611 | Show that the Ray relationship is a function. (Contributed by Scott Fenton, 21-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ Fun Ray | ||
Theorem | fvray 34612* | Calculate the value of the Ray function. (Contributed by Scott Fenton, 21-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π β π΄)) β (πRayπ΄) = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π΄, π₯β©}) | ||
Theorem | funline 34613 | Show that the Line relationship is a function. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ Fun Line | ||
Theorem | linedegen 34614 | When Line is applied with the same argument, the result is the empty set. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (π΄Lineπ΄) = β | ||
Theorem | fvline 34615* | Calculate the value of the Line function. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β (π΄Lineπ΅) = {π₯ β£ π₯ Colinear β¨π΄, π΅β©}) | ||
Theorem | liness 34616 | A line is a subset of the space its two points lie in. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β (π΄Lineπ΅) β (πΌβπ)) | ||
Theorem | fvline2 34617* | Alternate definition of a line. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β (π΄Lineπ΅) = {π₯ β (πΌβπ) β£ π₯ Colinear β¨π΄, π΅β©}) | ||
Theorem | lineunray 34618 | A line is composed of a point and the two rays emerging from it. Theorem 6.15 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 26-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ)) β§ (π β π β§ π β π )) β (π Btwn β¨π, π β© β (πLineπ) = (((πRayπ) βͺ {π}) βͺ (πRayπ )))) | ||
Theorem | lineelsb2 34619 | If π lies on ππ, then ππ = ππ. Theorem 6.16 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ (π β (πΌβπ) β§ π β π)) β (π β (πLineπ) β (πLineπ) = (πLineπ))) | ||
Theorem | linerflx1 34620 | Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π)) β π β (πLineπ)) | ||
Theorem | linecom 34621 | Commutativity law for lines. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π)) β (πLineπ) = (πLineπ)) | ||
Theorem | linerflx2 34622 | Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π)) β π β (πLineπ)) | ||
Theorem | ellines 34623* | 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 34624 | 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 34625* | 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 34626* | 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 34627* | 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 34628* | 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 34629 | Declare the syntax for the forward difference operator. |
class β³ | ||
Definition | df-fwddif 34630* | 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 34631 | Declare the syntax for the nth forward difference operator. |
class
β³ | ||
Definition | df-fwddifn 34632* | Define the nth forward difference operator. This works out to be the forward difference operator iterated π times. (Contributed by Scott Fenton, 28-May-2020.) |
β’
β³ | ||
Theorem | fwddifval 34633 | Calculate the value of the forward difference operator at a point. (Contributed by Scott Fenton, 18-May-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π β π΄) & β’ (π β (π + 1) β π΄) β β’ (π β (( β³ βπΉ)βπ) = ((πΉβ(π + 1)) β (πΉβπ))) | ||
Theorem | fwddifnval 34634* | The value of the forward difference operator at a point. (Contributed by Scott Fenton, 28-May-2020.) |
β’ (π β π β β0) & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π β β) & β’ ((π β§ π β (0...π)) β (π + π) β π΄) β β’ (π β ((π β³ | ||
Theorem | fwddifn0 34635 | The value of the n-iterated forward difference operator at zero is just the function value. (Contributed by Scott Fenton, 28-May-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π β π΄) β β’ (π β ((0 β³ | ||
Theorem | fwddifnp1 34636* | The value of the n-iterated forward difference at a successor. (Contributed by Scott Fenton, 28-May-2020.) |
β’ (π β π β β0) & β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π β β) & β’ ((π β§ π β (0...(π + 1))) β (π + π) β π΄) β β’ (π β (((π + 1) β³ | ||
Theorem | rankung 34637 | The rank of the union of two sets. Closed form of rankun 9726. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ ((π΄ β π β§ π΅ β π) β (rankβ(π΄ βͺ π΅)) = ((rankβπ΄) βͺ (rankβπ΅))) | ||
Theorem | ranksng 34638 | The rank of a singleton. Closed form of ranksn 9724. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ (π΄ β π β (rankβ{π΄}) = suc (rankβπ΄)) | ||
Theorem | rankelg 34639 | The membership relation is inherited by the rank function. Closed form of rankel 9709. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ ((π΅ β π β§ π΄ β π΅) β (rankβπ΄) β (rankβπ΅)) | ||
Theorem | rankpwg 34640 | The rank of a power set. Closed form of rankpw 9713. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ (π΄ β π β (rankβπ« π΄) = suc (rankβπ΄)) | ||
Theorem | rank0 34641 | The rank of the empty set is β . (Contributed by Scott Fenton, 17-Jul-2015.) |
β’ (rankββ ) = β | ||
Theorem | rankeq1o 34642 | The only set with rank 1o is the singleton of the empty set. (Contributed by Scott Fenton, 17-Jul-2015.) |
β’ ((rankβπ΄) = 1o β π΄ = {β }) | ||
Syntax | chf 34643 | The constant Hf is a class. |
class Hf | ||
Definition | df-hf 34644 | 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 34645* | Membership in the hereditarily finite sets. (Contributed by Scott Fenton, 9-Jul-2015.) |
β’ (π΄ β Hf β βπ₯ β Ο π΄ β (π 1βπ₯)) | ||
Theorem | elhf2 34646 | Alternate form of membership in the hereditarily finite sets. (Contributed by Scott Fenton, 13-Jul-2015.) |
β’ π΄ β V β β’ (π΄ β Hf β (rankβπ΄) β Ο) | ||
Theorem | elhf2g 34647 | Hereditarily finiteness via rank. Closed form of elhf2 34646. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ (π΄ β π β (π΄ β Hf β (rankβπ΄) β Ο)) | ||
Theorem | 0hf 34648 | The empty set is a hereditarily finite set. (Contributed by Scott Fenton, 9-Jul-2015.) |
β’ β β Hf | ||
Theorem | hfun 34649 | The union of two HF sets is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ ((π΄ β Hf β§ π΅ β Hf ) β (π΄ βͺ π΅) β Hf ) | ||
Theorem | hfsn 34650 | The singleton of an HF set is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ (π΄ β Hf β {π΄} β Hf ) | ||
Theorem | hfadj 34651 | Adjoining one HF element to an HF set preserves HF status. (Contributed by Scott Fenton, 15-Jul-2015.) |
β’ ((π΄ β Hf β§ π΅ β Hf ) β (π΄ βͺ {π΅}) β Hf ) | ||
Theorem | hfelhf 34652 | Any member of an HF set is itself an HF set. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ ((π΄ β π΅ β§ π΅ β Hf ) β π΄ β Hf ) | ||
Theorem | hftr 34653 | The class of all hereditarily finite sets is transitive. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ Tr Hf | ||
Theorem | hfext 34654* | Extensionality for HF sets depends only on comparison of HF elements. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ ((π΄ β Hf β§ π΅ β Hf ) β (π΄ = π΅ β βπ₯ β Hf (π₯ β π΄ β π₯ β π΅))) | ||
Theorem | hfuni 34655 | The union of an HF set is itself hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ (π΄ β Hf β βͺ π΄ β Hf ) | ||
Theorem | hfpw 34656 | The power class of an HF set is hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ (π΄ β Hf β π« π΄ β Hf ) | ||
Theorem | hfninf 34657 | Ο is not hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
β’ Β¬ Ο β Hf | ||
Theorem | a1i14 34658 | Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.) |
β’ (π β (π β π)) β β’ (π β (π β (π β (π β π)))) | ||
Theorem | a1i24 34659 | Add two antecedents to a wff. Deduction associated with a1i13 27. (Contributed by Jeff Hankins, 5-Aug-2009.) |
β’ (π β (π β π)) β β’ (π β (π β (π β (π β π)))) | ||
Theorem | exp5d 34660 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ (((π β§ π) β§ π) β ((π β§ π) β π)) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp5g 34661 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ π) β (((π β§ π) β§ π) β π)) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp5k 34662 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ (π β (((π β§ (π β§ π)) β§ π) β π)) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp56 34663 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((((π β§ π) β§ π) β§ (π β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp58 34664 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ (((π β§ π) β§ ((π β§ π) β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp510 34665 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ (((π β§ π) β§ π) β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp511 34666 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ ((π β§ (π β§ π)) β§ π)) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | exp512 34667 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
β’ ((π β§ ((π β§ π) β§ (π β§ π))) β π) β β’ (π β (π β (π β (π β (π β π))))) | ||
Theorem | 3com12d 34668 | Commutation in consequent. Swap 1st and 2nd. (Contributed by Jeff Hankins, 17-Nov-2009.) |
β’ (π β (π β§ π β§ π)) β β’ (π β (π β§ π β§ π)) | ||
Theorem | imp5p 34669 | A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.) |
β’ (π β (π β (π β (π β (π β π))))) β β’ (π β (π β ((π β§ π β§ π) β π))) | ||
Theorem | imp5q 34670 | A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.) |
β’ (π β (π β (π β (π β (π β π))))) β β’ ((π β§ π) β ((π β§ π β§ π) β π)) | ||
Theorem | ecase13d 34671 | Deduction for elimination by cases. (Contributed by Jeff Hankins, 18-Aug-2009.) |
β’ (π β Β¬ π) & β’ (π β Β¬ π) & β’ (π β (π β¨ π β¨ π)) β β’ (π β π) | ||
Theorem | subtr 34672 | Transitivity of implicit substitution. (Contributed by Jeff Hankins, 13-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π & β’ β²π₯π & β’ (π₯ = π΄ β π = π) & β’ (π₯ = π΅ β π = π) β β’ ((π΄ β πΆ β§ π΅ β π·) β (π΄ = π΅ β π = π)) | ||
Theorem | subtr2 34673 | Transitivity of implicit substitution into a wff. (Contributed by Jeff Hankins, 19-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π & β’ β²π₯π & β’ (π₯ = π΄ β (π β π)) & β’ (π₯ = π΅ β (π β π)) β β’ ((π΄ β πΆ β§ π΅ β π·) β (π΄ = π΅ β (π β π))) | ||
Theorem | trer 34674* | 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 34675 | An equivalent membership condition for closed intervals. (Contributed by Jeff Hankins, 14-Jul-2009.) |
β’ ((π΄ β β* β§ π΅ β β*) β (πΆ β (π΄[,]π΅) β (πΆ β β* β§ π΄ β€ π΅ β§ (πΆ = π΄ β¨ (π΄ < πΆ β§ πΆ < π΅) β¨ πΆ = π΅)))) | ||
Theorem | finminlem 34676* | 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 34677* | 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 34678* | 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 34679* | 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 34680* | Lemma for nn0prpw 34681. Use strong induction to show that every positive integer has unique prime power divisors. (Contributed by Jeff Hankins, 28-Sep-2013.) |
β’ (π΄ β β β βπ β β (π < π΄ β βπ β β βπ β β Β¬ ((πβπ) β₯ π β (πβπ) β₯ π΄))) | ||
Theorem | nn0prpw 34681* | 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 34682 | Two equivalent expressions for the boundary of a topology. (Contributed by Jeff Hankins, 23-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄))) = (((clsβπ½)βπ΄) β ((intβπ½)βπ΄))) | ||
Theorem | opnbnd 34683 | A set is open iff it is disjoint from its boundary. (Contributed by Jeff Hankins, 23-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (π΄ β π½ β (π΄ β© (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄)))) = β )) | ||
Theorem | cldbnd 34684 | A set is closed iff it contains its boundary. (Contributed by Jeff Hankins, 1-Oct-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (π΄ β (Clsdβπ½) β (((clsβπ½)βπ΄) β© ((clsβπ½)β(π β π΄))) β π΄)) | ||
Theorem | ntruni 34685* | 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 34686 | A pairwise union of closures is the closure of the union. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π β§ π΅ β π) β ((clsβπ½)β(π΄ βͺ π΅)) = (((clsβπ½)βπ΄) βͺ ((clsβπ½)βπ΅))) | ||
Theorem | clsint2 34687* | 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 34688* | 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 34689* | 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 34690 | Two neighborhoods intersect to form a neighborhood of the intersection. (Contributed by Jeff Hankins, 31-Aug-2009.) |
β’ ((π½ β Top β§ π β ((neiβπ½)βπ΄) β§ π β ((neiβπ½)βπ΅)) β (π β© π) β ((neiβπ½)β(π΄ β© π΅))) | ||
Theorem | hmeoclda 34691 | Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.) (Revised by Mario Carneiro, 3-Jun-2014.) |
β’ (((π½ β Top β§ πΎ β Top β§ πΉ β (π½HomeoπΎ)) β§ π β (Clsdβπ½)) β (πΉ β π) β (ClsdβπΎ)) | ||
Theorem | hmeocldb 34692 | Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.) |
β’ (((π½ β Top β§ πΎ β Top β§ πΉ β (π½HomeoπΎ)) β§ π β (ClsdβπΎ)) β (β‘πΉ β π) β (Clsdβπ½)) | ||
Theorem | ivthALT 34693* | An alternate proof of the Intermediate Value Theorem ivth 24740 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 34694 | Extend class definition to include the "finer than" relation. |
class Fne | ||
Definition | df-fne 34695* | Define the fineness relation for covers. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ Fne = {β¨π₯, π¦β© β£ (βͺ π₯ = βͺ π¦ β§ βπ§ β π₯ π§ β βͺ (π¦ β© π« π§))} | ||
Theorem | fnerel 34696 | Fineness is a relation. (Contributed by Jeff Hankins, 28-Sep-2009.) |
β’ Rel Fne | ||
Theorem | isfne 34697* | 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 34698 | The predicate "π΅ is finer than π΄ " in terms of the topology generation function. (Contributed by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΄Fneπ΅ β (π = π β§ π΄ β (topGenβπ΅))) | ||
Theorem | isfne4b 34699 | 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 34700* | The predicate "π΅ is finer than π΄". (Contributed by Jeff Hankins, 28-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΅ β πΆ β (π΄Fneπ΅ β (π = π β§ βπ₯ β π΄ βπ¦ β π₯ βπ§ β π΅ (π¦ β π§ β§ π§ β π₯)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |