Theorem List for Intuitionistic Logic Explorer - 12601-12700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | eltg2b 12601* |
Membership in a topology generated by a basis. (Contributed by Mario
Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 10-Jan-2015.)
|
|
|
Theorem | eltg4i 12602 |
An open set in a topology generated by a basis is the union of all basic
open sets contained in it. (Contributed by Stefan O'Rear,
22-Feb-2015.)
|
|
|
Theorem | eltg3i 12603 |
The union of a set of basic open sets is in the generated topology.
(Contributed by Mario Carneiro, 30-Aug-2015.)
|
|
|
Theorem | eltg3 12604* |
Membership in a topology generated by a basis. (Contributed by NM,
15-Jul-2006.) (Revised by Jim Kingdon, 4-Mar-2023.)
|
|
|
Theorem | tgval3 12605* |
Alternate expression for the topology generated by a basis. Lemma 2.1
of [Munkres] p. 80. See also tgval 12596 and tgval2 12598. (Contributed by
NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.)
|
|
|
Theorem | tg1 12606 |
Property of a member of a topology generated by a basis. (Contributed
by NM, 20-Jul-2006.)
|
|
|
Theorem | tg2 12607* |
Property of a member of a topology generated by a basis. (Contributed
by NM, 20-Jul-2006.)
|
|
|
Theorem | bastg 12608 |
A member of a basis is a subset of the topology it generates.
(Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro,
10-Jan-2015.)
|
|
|
Theorem | unitg 12609 |
The topology generated by a basis is a topology on .
Importantly, this theorem means that we don't have to specify separately
the base set for the topological space generated by a basis. In other
words, any member of the class completely specifies the
basis it corresponds to. (Contributed by NM, 16-Jul-2006.) (Proof
shortened by OpenAI, 30-Mar-2020.)
|
|
|
Theorem | tgss 12610 |
Subset relation for generated topologies. (Contributed by NM,
7-May-2007.)
|
|
|
Theorem | tgcl 12611 |
Show that a basis generates a topology. Remark in [Munkres] p. 79.
(Contributed by NM, 17-Jul-2006.)
|
|
|
Theorem | tgclb 12612 |
The property tgcl 12611 can be reversed: if the topology generated
by
is actually a topology, then must be a topological basis. This
yields an alternative definition of . (Contributed by
Mario Carneiro, 2-Sep-2015.)
|
|
|
Theorem | tgtopon 12613 |
A basis generates a topology on .
(Contributed by Mario
Carneiro, 14-Aug-2015.)
|
TopOn |
|
Theorem | topbas 12614 |
A topology is its own basis. (Contributed by NM, 17-Jul-2006.)
|
|
|
Theorem | tgtop 12615 |
A topology is its own basis. (Contributed by NM, 18-Jul-2006.)
|
|
|
Theorem | eltop 12616 |
Membership in a topology, expressed without quantifiers. (Contributed
by NM, 19-Jul-2006.)
|
|
|
Theorem | eltop2 12617* |
Membership in a topology. (Contributed by NM, 19-Jul-2006.)
|
|
|
Theorem | eltop3 12618* |
Membership in a topology. (Contributed by NM, 19-Jul-2006.)
|
|
|
Theorem | tgdom 12619 |
A space has no more open sets than subsets of a basis. (Contributed by
Stefan O'Rear, 22-Feb-2015.) (Revised by Mario Carneiro,
9-Apr-2015.)
|
|
|
Theorem | tgiun 12620* |
The indexed union of a set of basic open sets is in the generated
topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
|
|
|
Theorem | tgidm 12621 |
The topology generator function is idempotent. (Contributed by NM,
18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.)
|
|
|
Theorem | bastop 12622 |
Two ways to express that a basis is a topology. (Contributed by NM,
18-Jul-2006.)
|
|
|
Theorem | tgtop11 12623 |
The topology generation function is one-to-one when applied to completed
topologies. (Contributed by NM, 18-Jul-2006.)
|
|
|
Theorem | en1top 12624 |
is the only topology
with one element. (Contributed by FL,
18-Aug-2008.)
|
|
|
Theorem | tgss3 12625 |
A criterion for determining whether one topology is finer than another.
Lemma 2.2 of [Munkres] p. 80 using
abbreviations. (Contributed by NM,
20-Jul-2006.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
|
|
|
Theorem | tgss2 12626* |
A criterion for determining whether one topology is finer than another,
based on a comparison of their bases. Lemma 2.2 of [Munkres] p. 80.
(Contributed by NM, 20-Jul-2006.) (Proof shortened by Mario Carneiro,
2-Sep-2015.)
|
|
|
Theorem | basgen 12627 |
Given a topology ,
show that a subset
satisfying the third
antecedent is a basis for it. Lemma 2.3 of [Munkres] p. 81 using
abbreviations. (Contributed by NM, 22-Jul-2006.) (Revised by Mario
Carneiro, 2-Sep-2015.)
|
|
|
Theorem | basgen2 12628* |
Given a topology ,
show that a subset
satisfying the third
antecedent is a basis for it. Lemma 2.3 of [Munkres] p. 81.
(Contributed by NM, 20-Jul-2006.) (Proof shortened by Mario Carneiro,
2-Sep-2015.)
|
|
|
Theorem | 2basgeng 12629 |
Conditions that determine the equality of two generated topologies.
(Contributed by NM, 8-May-2007.) (Revised by Jim Kingdon,
5-Mar-2023.)
|
|
|
Theorem | bastop1 12630* |
A subset of a topology is a basis for the topology iff every member of
the topology is a union of members of the basis. We use the
idiom " " to express
" is a basis for
topology
" since we do not have a separate notation for this.
Definition 15.35 of [Schechter] p.
428. (Contributed by NM,
2-Feb-2008.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
|
|
|
Theorem | bastop2 12631* |
A version of bastop1 12630 that doesn't have in the antecedent.
(Contributed by NM, 3-Feb-2008.)
|
|
|
7.1.3 Examples of topologies
|
|
Theorem | distop 12632 |
The discrete topology on a set . Part of Example 2 in [Munkres]
p. 77. (Contributed by FL, 17-Jul-2006.) (Revised by Mario Carneiro,
19-Mar-2015.)
|
|
|
Theorem | topnex 12633 |
The class of all topologies is a proper class. The proof uses
discrete topologies and pwnex 4421. (Contributed by BJ, 2-May-2021.)
|
|
|
Theorem | distopon 12634 |
The discrete topology on a set , with base set. (Contributed by
Mario Carneiro, 13-Aug-2015.)
|
TopOn |
|
Theorem | sn0topon 12635 |
The singleton of the empty set is a topology on the empty set.
(Contributed by Mario Carneiro, 13-Aug-2015.)
|
TopOn |
|
Theorem | sn0top 12636 |
The singleton of the empty set is a topology. (Contributed by Stefan
Allan, 3-Mar-2006.) (Proof shortened by Mario Carneiro,
13-Aug-2015.)
|
|
|
Theorem | epttop 12637* |
The excluded point topology. (Contributed by Mario Carneiro,
3-Sep-2015.)
|
TopOn |
|
Theorem | distps 12638 |
The discrete topology on a set expressed as a topological space.
(Contributed by FL, 20-Aug-2006.)
|
TopSet |
|
7.1.4 Closure and interior
|
|
Syntax | ccld 12639 |
Extend class notation with the set of closed sets of a topology.
|
|
|
Syntax | cnt 12640 |
Extend class notation with interior of a subset of a topology base set.
|
|
|
Syntax | ccl 12641 |
Extend class notation with closure of a subset of a topology base set.
|
|
|
Definition | df-cld 12642* |
Define a function on topologies whose value is the set of closed sets of
the topology. (Contributed by NM, 2-Oct-2006.)
|
|
|
Definition | df-ntr 12643* |
Define a function on topologies whose value is the interior function on
the subsets of the base set. See ntrval 12657. (Contributed by NM,
10-Sep-2006.)
|
|
|
Definition | df-cls 12644* |
Define a function on topologies whose value is the closure function on
the subsets of the base set. See clsval 12658. (Contributed by NM,
3-Oct-2006.)
|
|
|
Theorem | fncld 12645 |
The closed-set generator is a well-behaved function. (Contributed by
Stefan O'Rear, 1-Feb-2015.)
|
|
|
Theorem | cldval 12646* |
The set of closed sets of a topology. (Note that the set of open sets
is just the topology itself, so we don't have a separate definition.)
(Contributed by NM, 2-Oct-2006.) (Revised by Mario Carneiro,
11-Nov-2013.)
|
|
|
Theorem | ntrfval 12647* |
The interior function on the subsets of a topology's base set.
(Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro,
11-Nov-2013.)
|
|
|
Theorem | clsfval 12648* |
The closure function on the subsets of a topology's base set.
(Contributed by NM, 3-Oct-2006.) (Revised by Mario Carneiro,
11-Nov-2013.)
|
|
|
Theorem | cldrcl 12649 |
Reverse closure of the closed set operation. (Contributed by Stefan
O'Rear, 22-Feb-2015.)
|
|
|
Theorem | iscld 12650 |
The predicate "the class is a closed set". (Contributed by NM,
2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|
|
|
Theorem | iscld2 12651 |
A subset of the underlying set of a topology is closed iff its
complement is open. (Contributed by NM, 4-Oct-2006.)
|
|
|
Theorem | cldss 12652 |
A closed set is a subset of the underlying set of a topology.
(Contributed by NM, 5-Oct-2006.) (Revised by Stefan O'Rear,
22-Feb-2015.)
|
|
|
Theorem | cldss2 12653 |
The set of closed sets is contained in the powerset of the base.
(Contributed by Mario Carneiro, 6-Jan-2014.)
|
|
|
Theorem | cldopn 12654 |
The complement of a closed set is open. (Contributed by NM,
5-Oct-2006.) (Revised by Stefan O'Rear, 22-Feb-2015.)
|
|
|
Theorem | difopn 12655 |
The difference of a closed set with an open set is open. (Contributed
by Mario Carneiro, 6-Jan-2014.)
|
|
|
Theorem | topcld 12656 |
The underlying set of a topology is closed. Part of Theorem 6.1(1) of
[Munkres] p. 93. (Contributed by NM,
3-Oct-2006.)
|
|
|
Theorem | ntrval 12657 |
The interior of a subset of a topology's base set is the union of all
the open sets it includes. Definition of interior of [Munkres] p. 94.
(Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro,
11-Nov-2013.)
|
|
|
Theorem | clsval 12658* |
The closure of a subset of a topology's base set is the intersection of
all the closed sets that include it. Definition of closure of [Munkres]
p. 94. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro,
11-Nov-2013.)
|
|
|
Theorem | 0cld 12659 |
The empty set is closed. Part of Theorem 6.1(1) of [Munkres] p. 93.
(Contributed by NM, 4-Oct-2006.)
|
|
|
Theorem | uncld 12660 |
The union of two closed sets is closed. Equivalent to Theorem 6.1(3) of
[Munkres] p. 93. (Contributed by NM,
5-Oct-2006.)
|
|
|
Theorem | cldcls 12661 |
A closed subset equals its own closure. (Contributed by NM,
15-Mar-2007.)
|
|
|
Theorem | iuncld 12662* |
A finite indexed union of closed sets is closed. (Contributed by Mario
Carneiro, 19-Sep-2015.) (Revised by Jim Kingdon, 10-Mar-2023.)
|
|
|
Theorem | unicld 12663 |
A finite union of closed sets is closed. (Contributed by Mario
Carneiro, 19-Sep-2015.)
|
|
|
Theorem | ntropn 12664 |
The interior of a subset of a topology's underlying set is open.
(Contributed by NM, 11-Sep-2006.) (Revised by Mario Carneiro,
11-Nov-2013.)
|
|
|
Theorem | clsss 12665 |
Subset relationship for closure. (Contributed by NM, 10-Feb-2007.)
|
|
|
Theorem | ntrss 12666 |
Subset relationship for interior. (Contributed by NM, 3-Oct-2007.)
(Revised by Jim Kingdon, 11-Mar-2023.)
|
|
|
Theorem | sscls 12667 |
A subset of a topology's underlying set is included in its closure.
(Contributed by NM, 22-Feb-2007.)
|
|
|
Theorem | ntrss2 12668 |
A subset includes its interior. (Contributed by NM, 3-Oct-2007.)
(Revised by Mario Carneiro, 11-Nov-2013.)
|
|
|
Theorem | ssntr 12669 |
An open subset of a set is a subset of the set's interior. (Contributed
by Jeff Hankins, 31-Aug-2009.) (Revised by Mario Carneiro,
11-Nov-2013.)
|
|
|
Theorem | ntrss3 12670 |
The interior of a subset of a topological space is included in the
space. (Contributed by NM, 1-Oct-2007.)
|
|
|
Theorem | ntrin 12671 |
A pairwise intersection of interiors is the interior of the
intersection. This does not always hold for arbitrary intersections.
(Contributed by Jeff Hankins, 31-Aug-2009.)
|
|
|
Theorem | isopn3 12672 |
A subset is open iff it equals its own interior. (Contributed by NM,
9-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|
|
|
Theorem | ntridm 12673 |
The interior operation is idempotent. (Contributed by NM,
2-Oct-2007.)
|
|
|
Theorem | clstop 12674 |
The closure of a topology's underlying set is the entire set.
(Contributed by NM, 5-Oct-2007.) (Proof shortened by Jim Kingdon,
11-Mar-2023.)
|
|
|
Theorem | ntrtop 12675 |
The interior of a topology's underlying set is the entire set.
(Contributed by NM, 12-Sep-2006.)
|
|
|
Theorem | clsss2 12676 |
If a subset is included in a closed set, so is the subset's closure.
(Contributed by NM, 22-Feb-2007.)
|
|
|
Theorem | clsss3 12677 |
The closure of a subset of a topological space is included in the space.
(Contributed by NM, 26-Feb-2007.)
|
|
|
Theorem | ntrcls0 12678 |
A subset whose closure has an empty interior also has an empty interior.
(Contributed by NM, 4-Oct-2007.)
|
|
|
Theorem | ntreq0 12679* |
Two ways to say that a subset has an empty interior. (Contributed by
NM, 3-Oct-2007.) (Revised by Jim Kingdon, 11-Mar-2023.)
|
|
|
Theorem | cls0 12680 |
The closure of the empty set. (Contributed by NM, 2-Oct-2007.) (Proof
shortened by Jim Kingdon, 12-Mar-2023.)
|
|
|
Theorem | ntr0 12681 |
The interior of the empty set. (Contributed by NM, 2-Oct-2007.)
|
|
|
Theorem | isopn3i 12682 |
An open subset equals its own interior. (Contributed by Mario Carneiro,
30-Dec-2016.)
|
|
|
Theorem | discld 12683 |
The open sets of a discrete topology are closed and its closed sets are
open. (Contributed by FL, 7-Jun-2007.) (Revised by Mario Carneiro,
7-Apr-2015.)
|
|
|
Theorem | sn0cld 12684 |
The closed sets of the topology .
(Contributed by FL,
5-Jan-2009.)
|
|
|
7.1.5 Neighborhoods
|
|
Syntax | cnei 12685 |
Extend class notation with neighborhood relation for topologies.
|
|
|
Definition | df-nei 12686* |
Define a function on topologies whose value is a map from a subset to
its neighborhoods. (Contributed by NM, 11-Feb-2007.)
|
|
|
Theorem | neifval 12687* |
Value of the neighborhood function on the subsets of the base set of a
topology. (Contributed by NM, 11-Feb-2007.) (Revised by Mario
Carneiro, 11-Nov-2013.)
|
|
|
Theorem | neif 12688 |
The neighborhood function is a function from the set of the subsets of
the base set of a topology. (Contributed by NM, 12-Feb-2007.) (Revised
by Mario Carneiro, 11-Nov-2013.)
|
|
|
Theorem | neiss2 12689 |
A set with a neighborhood is a subset of the base set of a topology.
(This theorem depends on a function's value being empty outside of its
domain, but it will make later theorems simpler to state.) (Contributed
by NM, 12-Feb-2007.)
|
|
|
Theorem | neival 12690* |
Value of the set of neighborhoods of a subset of the base set of a
topology. (Contributed by NM, 11-Feb-2007.) (Revised by Mario
Carneiro, 11-Nov-2013.)
|
|
|
Theorem | isnei 12691* |
The predicate "the class is a neighborhood of ".
(Contributed by FL, 25-Sep-2006.) (Revised by Mario Carneiro,
11-Nov-2013.)
|
|
|
Theorem | neiint 12692 |
An intuitive definition of a neighborhood in terms of interior.
(Contributed by Szymon Jaroszewicz, 18-Dec-2007.) (Revised by Mario
Carneiro, 11-Nov-2013.)
|
|
|
Theorem | isneip 12693* |
The predicate "the class is a neighborhood of point ".
(Contributed by NM, 26-Feb-2007.)
|
|
|
Theorem | neii1 12694 |
A neighborhood is included in the topology's base set. (Contributed by
NM, 12-Feb-2007.)
|
|
|
Theorem | neisspw 12695 |
The neighborhoods of any set are subsets of the base set. (Contributed
by Stefan O'Rear, 6-Aug-2015.)
|
|
|
Theorem | neii2 12696* |
Property of a neighborhood. (Contributed by NM, 12-Feb-2007.)
|
|
|
Theorem | neiss 12697 |
Any neighborhood of a set is also a neighborhood of any subset
. Similar to Proposition 1 of [BourbakiTop1] p. I.2.
(Contributed by FL, 25-Sep-2006.)
|
|
|
Theorem | ssnei 12698 |
A set is included in any of its neighborhoods. Generalization to
subsets of elnei 12699. (Contributed by FL, 16-Nov-2006.)
|
|
|
Theorem | elnei 12699 |
A point belongs to any of its neighborhoods. Property Viii of
[BourbakiTop1] p. I.3. (Contributed
by FL, 28-Sep-2006.)
|
|
|
Theorem | 0nnei 12700 |
The empty set is not a neighborhood of a nonempty set. (Contributed by
FL, 18-Sep-2007.)
|
|