Theorem List for Intuitionistic Logic Explorer - 11801-11900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | fiinbas 11801* |
If a set is closed under finite intersection, then it is a basis for a
topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
|
⊢ ((𝐵 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵) → 𝐵 ∈ TopBases) |
|
Theorem | baspartn 11802* |
A disjoint system of sets is a basis for a topology. (Contributed by
Stefan O'Rear, 22-Feb-2015.)
|
⊢ ((𝑃 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → 𝑃 ∈ TopBases) |
|
Theorem | tgval 11803* |
The topology generated by a basis. See also tgval2 11805 and tgval3 11812.
(Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro,
10-Jan-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)}) |
|
Theorem | tgvalex 11804 |
The topology generated by a basis is a set. (Contributed by Jim
Kingdon, 4-Mar-2023.)
|
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) ∈ V) |
|
Theorem | tgval2 11805* |
Definition of a topology generated by a basis in [Munkres] p. 78. Later
we show (in tgcl 11818) that (topGen‘𝐵) is indeed a topology
(on
∪ 𝐵, see unitg 11816). See also tgval 11803 and tgval3 11812. (Contributed
by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ (𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐵 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))}) |
|
Theorem | eltg 11806 |
Membership in a topology generated by a basis. (Contributed by NM,
16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ 𝐴 ⊆ ∪
(𝐵 ∩ 𝒫 𝐴))) |
|
Theorem | eltg2 11807* |
Membership in a topology generated by a basis. (Contributed by NM,
15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ (𝐴 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))) |
|
Theorem | eltg2b 11808* |
Membership in a topology generated by a basis. (Contributed by Mario
Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 10-Jan-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴))) |
|
Theorem | eltg4i 11809 |
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.)
|
⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 = ∪ (𝐵 ∩ 𝒫 𝐴)) |
|
Theorem | eltg3i 11810 |
The union of a set of basic open sets is in the generated topology.
(Contributed by Mario Carneiro, 30-Aug-2015.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → ∪ 𝐴 ∈ (topGen‘𝐵)) |
|
Theorem | eltg3 11811* |
Membership in a topology generated by a basis. (Contributed by NM,
15-Jul-2006.) (Revised by Jim Kingdon, 4-Mar-2023.)
|
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∃𝑥(𝑥 ⊆ 𝐵 ∧ 𝐴 = ∪ 𝑥))) |
|
Theorem | tgval3 11812* |
Alternate expression for the topology generated by a basis. Lemma 2.1
of [Munkres] p. 80. See also tgval 11803 and tgval2 11805. (Contributed by
NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)}) |
|
Theorem | tg1 11813 |
Property of a member of a topology generated by a basis. (Contributed
by NM, 20-Jul-2006.)
|
⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 ⊆ ∪ 𝐵) |
|
Theorem | tg2 11814* |
Property of a member of a topology generated by a basis. (Contributed
by NM, 20-Jul-2006.)
|
⊢ ((𝐴 ∈ (topGen‘𝐵) ∧ 𝐶 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴)) |
|
Theorem | bastg 11815 |
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.)
|
⊢ (𝐵 ∈ 𝑉 → 𝐵 ⊆ (topGen‘𝐵)) |
|
Theorem | unitg 11816 |
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 TopBases
completely specifies the
basis it corresponds to. (Contributed by NM, 16-Jul-2006.) (Proof
shortened by OpenAI, 30-Mar-2020.)
|
⊢ (𝐵 ∈ 𝑉 → ∪
(topGen‘𝐵) = ∪ 𝐵) |
|
Theorem | tgss 11817 |
Subset relation for generated topologies. (Contributed by NM,
7-May-2007.)
|
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶) → (topGen‘𝐵) ⊆ (topGen‘𝐶)) |
|
Theorem | tgcl 11818 |
Show that a basis generates a topology. Remark in [Munkres] p. 79.
(Contributed by NM, 17-Jul-2006.)
|
⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top) |
|
Theorem | tgclb 11819 |
The property tgcl 11818 can be reversed: if the topology generated
by 𝐵
is actually a topology, then 𝐵 must be a topological basis. This
yields an alternative definition of TopBases.
(Contributed by
Mario Carneiro, 2-Sep-2015.)
|
⊢ (𝐵 ∈ TopBases ↔ (topGen‘𝐵) ∈ Top) |
|
Theorem | tgtopon 11820 |
A basis generates a topology on ∪
𝐵. (Contributed by
Mario
Carneiro, 14-Aug-2015.)
|
⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ (TopOn‘∪ 𝐵)) |
|
Theorem | topbas 11821 |
A topology is its own basis. (Contributed by NM, 17-Jul-2006.)
|
⊢ (𝐽 ∈ Top → 𝐽 ∈ TopBases) |
|
Theorem | tgtop 11822 |
A topology is its own basis. (Contributed by NM, 18-Jul-2006.)
|
⊢ (𝐽 ∈ Top → (topGen‘𝐽) = 𝐽) |
|
Theorem | eltop 11823 |
Membership in a topology, expressed without quantifiers. (Contributed
by NM, 19-Jul-2006.)
|
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ 𝐴 ⊆ ∪
(𝐽 ∩ 𝒫 𝐴))) |
|
Theorem | eltop2 11824* |
Membership in a topology. (Contributed by NM, 19-Jul-2006.)
|
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴))) |
|
Theorem | eltop3 11825* |
Membership in a topology. (Contributed by NM, 19-Jul-2006.)
|
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∃𝑥(𝑥 ⊆ 𝐽 ∧ 𝐴 = ∪ 𝑥))) |
|
Theorem | tgdom 11826 |
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.)
|
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) ≼ 𝒫 𝐵) |
|
Theorem | tgiun 11827* |
The indexed union of a set of basic open sets is in the generated
topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵) → ∪ 𝑥 ∈ 𝐴 𝐶 ∈ (topGen‘𝐵)) |
|
Theorem | tgidm 11828 |
The topology generator function is idempotent. (Contributed by NM,
18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.)
|
⊢ (𝐵 ∈ 𝑉 → (topGen‘(topGen‘𝐵)) = (topGen‘𝐵)) |
|
Theorem | bastop 11829 |
Two ways to express that a basis is a topology. (Contributed by NM,
18-Jul-2006.)
|
⊢ (𝐵 ∈ TopBases → (𝐵 ∈ Top ↔ (topGen‘𝐵) = 𝐵)) |
|
Theorem | tgtop11 11830 |
The topology generation function is one-to-one when applied to completed
topologies. (Contributed by NM, 18-Jul-2006.)
|
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ (topGen‘𝐽) = (topGen‘𝐾)) → 𝐽 = 𝐾) |
|
Theorem | en1top 11831 |
{∅} is the only topology with one element.
(Contributed by FL,
18-Aug-2008.)
|
⊢ (𝐽 ∈ Top → (𝐽 ≈ 1o ↔ 𝐽 = {∅})) |
|
Theorem | tgss3 11832 |
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.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → ((topGen‘𝐵) ⊆ (topGen‘𝐶) ↔ 𝐵 ⊆ (topGen‘𝐶))) |
|
Theorem | tgss2 11833* |
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.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ ∪ 𝐵 = ∪
𝐶) →
((topGen‘𝐵) ⊆
(topGen‘𝐶) ↔
∀𝑥 ∈ ∪ 𝐵∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 → ∃𝑧 ∈ 𝐶 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)))) |
|
Theorem | basgen 11834 |
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.)
|
⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ 𝐽 ⊆ (topGen‘𝐵)) → (topGen‘𝐵) = 𝐽) |
|
Theorem | basgen2 11835* |
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.)
|
⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐵 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥)) → (topGen‘𝐵) = 𝐽) |
|
Theorem | 2basgeng 11836 |
Conditions that determine the equality of two generated topologies.
(Contributed by NM, 8-May-2007.) (Revised by Jim Kingdon,
5-Mar-2023.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ (topGen‘𝐵)) → (topGen‘𝐵) = (topGen‘𝐶)) |
|
Theorem | bastop1 11837* |
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 "(topGen‘𝐵) = 𝐽 " 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.)
|
⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽) → ((topGen‘𝐵) = 𝐽 ↔ ∀𝑥 ∈ 𝐽 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))) |
|
Theorem | bastop2 11838* |
A version of bastop1 11837 that doesn't have 𝐵 ⊆ 𝐽 in the antecedent.
(Contributed by NM, 3-Feb-2008.)
|
⊢ (𝐽 ∈ Top → ((topGen‘𝐵) = 𝐽 ↔ (𝐵 ⊆ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)))) |
|
6.1.3 Examples of topologies
|
|
Theorem | distop 11839 |
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.)
|
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top) |
|
Theorem | topnex 11840 |
The class of all topologies is a proper class. The proof uses
discrete topologies and pwnex 4284. (Contributed by BJ, 2-May-2021.)
|
⊢ Top ∉ V |
|
Theorem | distopon 11841 |
The discrete topology on a set 𝐴, with base set. (Contributed by
Mario Carneiro, 13-Aug-2015.)
|
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴)) |
|
Theorem | sn0topon 11842 |
The singleton of the empty set is a topology on the empty set.
(Contributed by Mario Carneiro, 13-Aug-2015.)
|
⊢ {∅} ∈
(TopOn‘∅) |
|
Theorem | sn0top 11843 |
The singleton of the empty set is a topology. (Contributed by Stefan
Allan, 3-Mar-2006.) (Proof shortened by Mario Carneiro,
13-Aug-2015.)
|
⊢ {∅} ∈ Top |
|
Theorem | epttop 11844* |
The excluded point topology. (Contributed by Mario Carneiro,
3-Sep-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 → 𝑥 = 𝐴)} ∈ (TopOn‘𝐴)) |
|
Theorem | distps 11845 |
The discrete topology on a set 𝐴 expressed as a topological space.
(Contributed by FL, 20-Aug-2006.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐾 = {〈(Base‘ndx),
𝐴〉,
〈(TopSet‘ndx), 𝒫 𝐴〉} ⇒ ⊢ 𝐾 ∈ TopSp |
|
6.1.4 Closure and interior
|
|
Syntax | ccld 11846 |
Extend class notation with the set of closed sets of a topology.
|
class Clsd |
|
Syntax | cnt 11847 |
Extend class notation with interior of a subset of a topology base set.
|
class int |
|
Syntax | ccl 11848 |
Extend class notation with closure of a subset of a topology base set.
|
class cls |
|
Definition | df-cld 11849* |
Define a function on topologies whose value is the set of closed sets of
the topology. (Contributed by NM, 2-Oct-2006.)
|
⊢ Clsd = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗
∣ (∪ 𝑗 ∖ 𝑥) ∈ 𝑗}) |
|
Definition | df-ntr 11850* |
Define a function on topologies whose value is the interior function on
the subsets of the base set. See ntrval 11864. (Contributed by NM,
10-Sep-2006.)
|
⊢ int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∪ (𝑗 ∩ 𝒫 𝑥))) |
|
Definition | df-cls 11851* |
Define a function on topologies whose value is the closure function on
the subsets of the base set. See clsval 11865. (Contributed by NM,
3-Oct-2006.)
|
⊢ cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦})) |
|
Theorem | fncld 11852 |
The closed-set generator is a well-behaved function. (Contributed by
Stefan O'Rear, 1-Feb-2015.)
|
⊢ Clsd Fn Top |
|
Theorem | cldval 11853* |
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.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ∈ 𝐽}) |
|
Theorem | ntrfval 11854* |
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.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (int‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ ∪
(𝐽 ∩ 𝒫 𝑥))) |
|
Theorem | clsfval 11855* |
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.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (cls‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ ∩
{𝑦 ∈
(Clsd‘𝐽) ∣
𝑥 ⊆ 𝑦})) |
|
Theorem | cldrcl 11856 |
Reverse closure of the closed set operation. (Contributed by Stefan
O'Rear, 22-Feb-2015.)
|
⊢ (𝐶 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) |
|
Theorem | iscld 11857 |
The predicate "the class 𝑆 is a closed set". (Contributed
by NM,
2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑆 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑆) ∈ 𝐽))) |
|
Theorem | iscld2 11858 |
A subset of the underlying set of a topology is closed iff its
complement is open. (Contributed by NM, 4-Oct-2006.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑋 ∖ 𝑆) ∈ 𝐽)) |
|
Theorem | cldss 11859 |
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.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ⊆ 𝑋) |
|
Theorem | cldss2 11860 |
The set of closed sets is contained in the powerset of the base.
(Contributed by Mario Carneiro, 6-Jan-2014.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (Clsd‘𝐽) ⊆ 𝒫 𝑋 |
|
Theorem | cldopn 11861 |
The complement of a closed set is open. (Contributed by NM,
5-Oct-2006.) (Revised by Stefan O'Rear, 22-Feb-2015.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝑆 ∈ (Clsd‘𝐽) → (𝑋 ∖ 𝑆) ∈ 𝐽) |
|
Theorem | difopn 11862 |
The difference of a closed set with an open set is open. (Contributed
by Mario Carneiro, 6-Jan-2014.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ (Clsd‘𝐽)) → (𝐴 ∖ 𝐵) ∈ 𝐽) |
|
Theorem | topcld 11863 |
The underlying set of a topology is closed. Part of Theorem 6.1(1) of
[Munkres] p. 93. (Contributed by NM,
3-Oct-2006.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → 𝑋 ∈ (Clsd‘𝐽)) |
|
Theorem | ntrval 11864 |
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.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) = ∪ (𝐽 ∩ 𝒫 𝑆)) |
|
Theorem | clsval 11865* |
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.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑥}) |
|
Theorem | 0cld 11866 |
The empty set is closed. Part of Theorem 6.1(1) of [Munkres] p. 93.
(Contributed by NM, 4-Oct-2006.)
|
⊢ (𝐽 ∈ Top → ∅ ∈
(Clsd‘𝐽)) |
|
Theorem | uncld 11867 |
The union of two closed sets is closed. Equivalent to Theorem 6.1(3) of
[Munkres] p. 93. (Contributed by NM,
5-Oct-2006.)
|
⊢ ((𝐴 ∈ (Clsd‘𝐽) ∧ 𝐵 ∈ (Clsd‘𝐽)) → (𝐴 ∪ 𝐵) ∈ (Clsd‘𝐽)) |
|
Theorem | cldcls 11868 |
A closed subset equals its own closure. (Contributed by NM,
15-Mar-2007.)
|
⊢ (𝑆 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘𝑆) = 𝑆) |
|
Theorem | iuncld 11869* |
A finite indexed union of closed sets is closed. (Contributed by Mario
Carneiro, 19-Sep-2015.) (Revised by Jim Kingdon, 10-Mar-2023.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) |
|
Theorem | unicld 11870 |
A finite union of closed sets is closed. (Contributed by Mario
Carneiro, 19-Sep-2015.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ (Clsd‘𝐽)) → ∪
𝐴 ∈ (Clsd‘𝐽)) |
|
Theorem | ntropn 11871 |
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.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ∈ 𝐽) |
|
Theorem | clsss 11872 |
Subset relationship for closure. (Contributed by NM, 10-Feb-2007.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((cls‘𝐽)‘𝑇) ⊆ ((cls‘𝐽)‘𝑆)) |
|
Theorem | ntrss 11873 |
Subset relationship for interior. (Contributed by NM, 3-Oct-2007.)
(Revised by Jim Kingdon, 11-Mar-2023.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((int‘𝐽)‘𝑇) ⊆ ((int‘𝐽)‘𝑆)) |
|
Theorem | sscls 11874 |
A subset of a topology's underlying set is included in its closure.
(Contributed by NM, 22-Feb-2007.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆)) |
|
Theorem | ntrss2 11875 |
A subset includes its interior. (Contributed by NM, 3-Oct-2007.)
(Revised by Mario Carneiro, 11-Nov-2013.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑆) |
|
Theorem | ssntr 11876 |
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.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑂 ∈ 𝐽 ∧ 𝑂 ⊆ 𝑆)) → 𝑂 ⊆ ((int‘𝐽)‘𝑆)) |
|
Theorem | ntrss3 11877 |
The interior of a subset of a topological space is included in the
space. (Contributed by NM, 1-Oct-2007.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑋) |
|
Theorem | ntrin 11878 |
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.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) → ((int‘𝐽)‘(𝐴 ∩ 𝐵)) = (((int‘𝐽)‘𝐴) ∩ ((int‘𝐽)‘𝐵))) |
|
Theorem | isopn3 11879 |
A subset is open iff it equals its own interior. (Contributed by NM,
9-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐽 ↔ ((int‘𝐽)‘𝑆) = 𝑆)) |
|
Theorem | ntridm 11880 |
The interior operation is idempotent. (Contributed by NM,
2-Oct-2007.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘((int‘𝐽)‘𝑆)) = ((int‘𝐽)‘𝑆)) |
|
Theorem | clstop 11881 |
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.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘𝑋) = 𝑋) |
|
Theorem | ntrtop 11882 |
The interior of a topology's underlying set is the entire set.
(Contributed by NM, 12-Sep-2006.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → ((int‘𝐽)‘𝑋) = 𝑋) |
|
Theorem | clsss2 11883 |
If a subset is included in a closed set, so is the subset's closure.
(Contributed by NM, 22-Feb-2007.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐶 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝐶) → ((cls‘𝐽)‘𝑆) ⊆ 𝐶) |
|
Theorem | clsss3 11884 |
The closure of a subset of a topological space is included in the space.
(Contributed by NM, 26-Feb-2007.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋) |
|
Theorem | ntrcls0 11885 |
A subset whose closure has an empty interior also has an empty interior.
(Contributed by NM, 4-Oct-2007.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ ((int‘𝐽)‘((cls‘𝐽)‘𝑆)) = ∅) → ((int‘𝐽)‘𝑆) = ∅) |
|
Theorem | ntreq0 11886* |
Two ways to say that a subset has an empty interior. (Contributed by
NM, 3-Oct-2007.) (Revised by Jim Kingdon, 11-Mar-2023.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (((int‘𝐽)‘𝑆) = ∅ ↔ ∀𝑥 ∈ 𝐽 (𝑥 ⊆ 𝑆 → 𝑥 = ∅))) |
|
Theorem | cls0 11887 |
The closure of the empty set. (Contributed by NM, 2-Oct-2007.) (Proof
shortened by Jim Kingdon, 12-Mar-2023.)
|
⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘∅) =
∅) |
|
Theorem | ntr0 11888 |
The interior of the empty set. (Contributed by NM, 2-Oct-2007.)
|
⊢ (𝐽 ∈ Top → ((int‘𝐽)‘∅) =
∅) |
|
Theorem | isopn3i 11889 |
An open subset equals its own interior. (Contributed by Mario Carneiro,
30-Dec-2016.)
|
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → ((int‘𝐽)‘𝑆) = 𝑆) |
|
Theorem | discld 11890 |
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.)
|
⊢ (𝐴 ∈ 𝑉 → (Clsd‘𝒫 𝐴) = 𝒫 𝐴) |
|
Theorem | sn0cld 11891 |
The closed sets of the topology {∅}.
(Contributed by FL,
5-Jan-2009.)
|
⊢ (Clsd‘{∅}) =
{∅} |
|
6.2 Metric spaces
|
|
6.2.1 Topological definitions using the
reals
|
|
Syntax | ccncf 11892 |
Extend class notation to include the operation which returns a class of
continuous complex functions.
|
class –cn→ |
|
Definition | df-cncf 11893* |
Define the operation whose value is a class of continuous complex
functions. (Contributed by Paul Chapman, 11-Oct-2007.)
|
⊢ –cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ
↦ {𝑓 ∈ (𝑏 ↑𝑚
𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)}) |
|
Theorem | cncfval 11894* |
The value of the continuous complex function operation is the set of
continuous functions from 𝐴 to 𝐵. (Contributed by Paul
Chapman, 11-Oct-2007.) (Revised by Mario Carneiro, 9-Nov-2013.)
|
⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐴–cn→𝐵) = {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑤))) < 𝑦)}) |
|
Theorem | elcncf 11895* |
Membership in the set of continuous complex functions from 𝐴 to
𝐵. (Contributed by Paul Chapman,
11-Oct-2007.) (Revised by Mario
Carneiro, 9-Nov-2013.)
|
⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))) |
|
Theorem | elcncf2 11896* |
Version of elcncf 11895 with arguments commuted. (Contributed by
Mario
Carneiro, 28-Apr-2014.)
|
⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑦)))) |
|
Theorem | cncfrss 11897 |
Reverse closure of the continuous function predicate. (Contributed by
Mario Carneiro, 25-Aug-2014.)
|
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ) |
|
Theorem | cncfrss2 11898 |
Reverse closure of the continuous function predicate. (Contributed by
Mario Carneiro, 25-Aug-2014.)
|
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ) |
|
Theorem | cncff 11899 |
A continuous complex function's domain and codomain. (Contributed by
Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro,
25-Aug-2014.)
|
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐹:𝐴⟶𝐵) |
|
Theorem | cncfi 11900* |
Defining property of a continuous function. (Contributed by Mario
Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.)
|
⊢ ((𝐹 ∈ (𝐴–cn→𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝑅 ∈ ℝ+) →
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝐶))) < 𝑅)) |