Home | Metamath
Proof Explorer Theorem List (p. 207 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tgss3 20601 | 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 20602* | 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 20603 | 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 20604* | 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 | 2basgen 20605 | Conditions that determine the equality of two generated topologies. (Contributed by NM, 8-May-2007.) (Revised by Mario Carneiro, 2-Sep-2015.) |
⊢ ((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ (topGen‘𝐵)) → (topGen‘𝐵) = (topGen‘𝐶)) | ||
Theorem | tgfiss 20606 | If a subbase is included into a topology, so is the generated topology. (Contributed by FL, 20-Apr-2012.) (Proof shortened by Mario Carneiro, 10-Jan-2015.) |
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽) → (topGen‘(fi‘𝐴)) ⊆ 𝐽) | ||
Theorem | tgdif0 20607 | A generated topology is not affected by the addition or removal of the empty set from the base. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ (topGen‘(𝐵 ∖ {∅})) = (topGen‘𝐵) | ||
Theorem | bastop1 20608* | 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 20609* | A version of bastop1 20608 that doesn't have 𝐵 ⊆ 𝐽 in the antecedent. (Contributed by NM, 3-Feb-2008.) |
⊢ (𝐽 ∈ Top → ((topGen‘𝐵) = 𝐽 ↔ (𝐵 ⊆ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)))) | ||
Theorem | distop 20610 | 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 | distopon 20611 | The discrete topology on a set 𝐴, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴)) | ||
Theorem | sn0topon 20612 | The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ {∅} ∈ (TopOn‘∅) | ||
Theorem | sn0top 20613 | 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 | indislem 20614 | A lemma to eliminate some sethood hypotheses when dealing with the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ {∅, ( I ‘𝐴)} = {∅, 𝐴} | ||
Theorem | indistopon 20615 | The indiscrete topology on a set 𝐴. Part of Example 2 in [Munkres] p. 77. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐴 ∈ 𝑉 → {∅, 𝐴} ∈ (TopOn‘𝐴)) | ||
Theorem | indistop 20616 | The indiscrete topology on a set 𝐴. Part of Example 2 in [Munkres] p. 77. (Contributed by FL, 16-Jul-2006.) (Revised by Stefan Allan, 6-Nov-2008.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ {∅, 𝐴} ∈ Top | ||
Theorem | indisuni 20617 | The base set of the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ ( I ‘𝐴) = ∪ {∅, 𝐴} | ||
Theorem | fctop 20618* | The finite complement topology on a set 𝐴. Example 3 in [Munkres] p. 77. (Contributed by FL, 15-Aug-2006.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴)) | ||
Theorem | fctop2 20619* | The finite complement topology on a set 𝐴. Example 3 in [Munkres] p. 77. (This version of fctop 20618 requires the Axiom of Infinity.) (Contributed by FL, 20-Aug-2006.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≺ ω ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴)) | ||
Theorem | cctop 20620* | The countable complement topology on a set 𝐴. Example 4 in [Munkres] p. 77. (Contributed by FL, 23-Aug-2006.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴)) | ||
Theorem | ppttop 20621* | The particular point topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴)) | ||
Theorem | pptbas 20622* | The particular point topology is generated by a basis consisting of pairs {𝑥, 𝑃} for each 𝑥 ∈ 𝐴. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} = (topGen‘ran (𝑥 ∈ 𝐴 ↦ {𝑥, 𝑃}))) | ||
Theorem | epttop 20623* | The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 → 𝑥 = 𝐴)} ∈ (TopOn‘𝐴)) | ||
Theorem | indistpsx 20624 | The indiscrete topology on a set 𝐴 expressed as a topological space, using explicit structure component references. Compare with indistps 20625 and indistps2 20626. The advantage of this version is that the actual function for the structure is evident, and df-ndx 15698 is not needed, nor any other special definition outside of basic set theory. The disadvantage is that if the indices of the component definitions df-base 15700 and df-tset 15787 are changed in the future, this theorem will also have to be changed. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use indistps 20625 instead. (New usage is discouraged.) (Contributed by FL, 19-Jul-2006.) |
⊢ 𝐴 ∈ V & ⊢ 𝐾 = {〈1, 𝐴〉, 〈9, {∅, 𝐴}〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | indistps 20625 | The indiscrete topology on a set 𝐴 expressed as a topological space, using implicit structure indices. The advantage of this version over indistpsx 20624 is that it is independent of the indices of the component definitions df-base 15700 and df-tset 15787, and if they are changed in the future, this theorem will not be affected. The advantage over indistps2 20626 is that it is easy to eliminate the hypotheses with eqid 2610 and vtoclg 3239 to result in a closed theorem. Theorems indistpsALT 20627 and indistps2ALT 20628 show that the two forms can be derived from each other. (Contributed by FL, 19-Jul-2006.) |
⊢ 𝐴 ∈ V & ⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), {∅, 𝐴}〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | indistps2 20626 | The indiscrete topology on a set 𝐴 expressed as a topological space, using direct component assignments. Compare with indistps 20625. The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT 20627 and indistps2ALT 20628 show that the two forms can be derived from each other. (Contributed by NM, 24-Oct-2012.) |
⊢ (Base‘𝐾) = 𝐴 & ⊢ (TopOpen‘𝐾) = {∅, 𝐴} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | indistpsALT 20627 | The indiscrete topology on a set 𝐴 expressed as a topological space. Here we show how to derive the structural version indistps 20625 from the direct component assignment version indistps2 20626. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), {∅, 𝐴}〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | indistps2ALT 20628 | The indiscrete topology on a set 𝐴 expressed as a topological space, using direct component assignments. Here we show how to derive the direct component assignment version indistps2 20626 from the structural version indistps 20625. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (Base‘𝐾) = 𝐴 & ⊢ (TopOpen‘𝐾) = {∅, 𝐴} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | distps 20629 | The discrete topology on a set 𝐴 expressed as a topological space. (Contributed by FL, 20-Aug-2006.) |
⊢ 𝐴 ∈ V & ⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), 𝒫 𝐴〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Syntax | ccld 20630 | Extend class notation with the set of closed sets of a topology. |
class Clsd | ||
Syntax | cnt 20631 | Extend class notation with interior of a subset of a topology base set. |
class int | ||
Syntax | ccl 20632 | Extend class notation with closure of a subset of a topology base set. |
class cls | ||
Definition | df-cld 20633* | 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 20634* | Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 20650. (Contributed by NM, 10-Sep-2006.) |
⊢ int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥))) | ||
Definition | df-cls 20635* | Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 20651. (Contributed by NM, 3-Oct-2006.) |
⊢ cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦})) | ||
Theorem | fncld 20636 | The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ Clsd Fn Top | ||
Theorem | cldval 20637* | 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 20638* | 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 20639* | 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 20640 | Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (𝐶 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) | ||
Theorem | iscld 20641 | The predicate "𝑆 is a closed set." (Contributed by NM, 2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑆 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑆) ∈ 𝐽))) | ||
Theorem | iscld2 20642 | 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 20643 | 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 20644 | The set of closed sets is contained in the powerset of the base. (Contributed by Mario Carneiro, 6-Jan-2014.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (Clsd‘𝐽) ⊆ 𝒫 𝑋 | ||
Theorem | cldopn 20645 | The complement of a closed set is open. (Contributed by NM, 5-Oct-2006.) (Revised by Stefan O'Rear, 22-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝑆 ∈ (Clsd‘𝐽) → (𝑋 ∖ 𝑆) ∈ 𝐽) | ||
Theorem | isopn2 20646 | A subset of the underlying set of a topology is open iff its complement is closed. (Contributed by NM, 4-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐽 ↔ (𝑋 ∖ 𝑆) ∈ (Clsd‘𝐽))) | ||
Theorem | opncld 20647 | The complement of an open set is closed. (Contributed by NM, 6-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → (𝑋 ∖ 𝑆) ∈ (Clsd‘𝐽)) | ||
Theorem | difopn 20648 | The difference of a closed set with an open set is open. (Contributed by Mario Carneiro, 6-Jan-2014.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ (Clsd‘𝐽)) → (𝐴 ∖ 𝐵) ∈ 𝐽) | ||
Theorem | topcld 20649 | 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 20650 | 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 20651* | 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 20652 | The empty set is closed. Part of Theorem 6.1(1) of [Munkres] p. 93. (Contributed by NM, 4-Oct-2006.) |
⊢ (𝐽 ∈ Top → ∅ ∈ (Clsd‘𝐽)) | ||
Theorem | iincld 20653* | The indexed intersection of a collection 𝐵(𝑥) of closed sets is closed. Theorem 6.1(2) of [Munkres] p. 93. (Contributed by NM, 5-Oct-2006.) (Revised by Mario Carneiro, 3-Sep-2015.) |
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) | ||
Theorem | intcld 20654 | The intersection of a set of closed sets is closed. (Contributed by NM, 5-Oct-2006.) |
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ (Clsd‘𝐽)) → ∩ 𝐴 ∈ (Clsd‘𝐽)) | ||
Theorem | uncld 20655 | 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 20656 | A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007.) |
⊢ (𝑆 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘𝑆) = 𝑆) | ||
Theorem | incld 20657 | The intersection of two closed sets is closed. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Sep-2015.) |
⊢ ((𝐴 ∈ (Clsd‘𝐽) ∧ 𝐵 ∈ (Clsd‘𝐽)) → (𝐴 ∩ 𝐵) ∈ (Clsd‘𝐽)) | ||
Theorem | riincld 20658* | An indexed relative intersection of closed sets is closed. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → (𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵) ∈ (Clsd‘𝐽)) | ||
Theorem | iuncld 20659* | A finite indexed union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) | ||
Theorem | unicld 20660 | A finite union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ (Clsd‘𝐽)) → ∪ 𝐴 ∈ (Clsd‘𝐽)) | ||
Theorem | clscld 20661 | The closure of a subset of a topology's underlying set is closed. (Contributed by NM, 4-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽)) | ||
Theorem | clsf 20662 | The closure function is a function from subsets of the base to closed sets. (Contributed by Mario Carneiro, 11-Apr-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (cls‘𝐽):𝒫 𝑋⟶(Clsd‘𝐽)) | ||
Theorem | ntropn 20663 | 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 | clsval2 20664 | Express closure in terms of interior. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = (𝑋 ∖ ((int‘𝐽)‘(𝑋 ∖ 𝑆)))) | ||
Theorem | ntrval2 20665 | Interior expressed in terms of closure. (Contributed by NM, 1-Oct-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) = (𝑋 ∖ ((cls‘𝐽)‘(𝑋 ∖ 𝑆)))) | ||
Theorem | ntrdif 20666 | An interior of a complement is the complement of the closure. This set is also known as the exterior of 𝐴. (Contributed by Jeff Hankins, 31-Aug-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐽)‘(𝑋 ∖ 𝐴)) = (𝑋 ∖ ((cls‘𝐽)‘𝐴))) | ||
Theorem | clsdif 20667 | A closure of a complement is the complement of the interior. (Contributed by Jeff Hankins, 31-Aug-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘(𝑋 ∖ 𝐴)) = (𝑋 ∖ ((int‘𝐽)‘𝐴))) | ||
Theorem | clsss 20668 | Subset relationship for closure. (Contributed by NM, 10-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((cls‘𝐽)‘𝑇) ⊆ ((cls‘𝐽)‘𝑆)) | ||
Theorem | ntrss 20669 | Subset relationship for interior. (Contributed by NM, 3-Oct-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((int‘𝐽)‘𝑇) ⊆ ((int‘𝐽)‘𝑆)) | ||
Theorem | sscls 20670 | A subset of a topology's underlying set is included in its closure. (Contributed by NM, 22-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆)) | ||
Theorem | ntrss2 20671 | A subset includes its interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑆) | ||
Theorem | ssntr 20672 | 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 | clsss3 20673 | The closure of a subset of a topological space is included in the space. (Contributed by NM, 26-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋) | ||
Theorem | ntrss3 20674 | The interior of a subset of a topological space is included in the space. (Contributed by NM, 1-Oct-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑋) | ||
Theorem | ntrin 20675 | 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 | cmclsopn 20676 | The complement of a closure is open. (Contributed by NM, 11-Sep-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∈ 𝐽) | ||
Theorem | cmntrcld 20677 | The complement of an interior is closed. (Contributed by NM, 1-Oct-2007.) (Proof shortened by OpenAI, 3-Jul-2020.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑋 ∖ ((int‘𝐽)‘𝑆)) ∈ (Clsd‘𝐽)) | ||
Theorem | iscld3 20678 | A subset is closed iff it equals its own closure. (Contributed by NM, 2-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((cls‘𝐽)‘𝑆) = 𝑆)) | ||
Theorem | iscld4 20679 | A subset is closed iff it contains its own closure. (Contributed by NM, 31-Jan-2008.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((cls‘𝐽)‘𝑆) ⊆ 𝑆)) | ||
Theorem | isopn3 20680 | 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 | clsidm 20681 | The closure operation is idempotent. (Contributed by NM, 2-Oct-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘((cls‘𝐽)‘𝑆)) = ((cls‘𝐽)‘𝑆)) | ||
Theorem | ntridm 20682 | The interior operation is idempotent. (Contributed by NM, 2-Oct-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘((int‘𝐽)‘𝑆)) = ((int‘𝐽)‘𝑆)) | ||
Theorem | clstop 20683 | The closure of a topology's underlying set is entire set. (Contributed by NM, 5-Oct-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘𝑋) = 𝑋) | ||
Theorem | ntrtop 20684 | The interior of a topology's underlying set is entire set. (Contributed by NM, 12-Sep-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → ((int‘𝐽)‘𝑋) = 𝑋) | ||
Theorem | 0ntr 20685 | A subset with an empty interior cannot cover a whole (nonempty) topology. (Contributed by NM, 12-Sep-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝑋 ≠ ∅) ∧ (𝑆 ⊆ 𝑋 ∧ ((int‘𝐽)‘𝑆) = ∅)) → (𝑋 ∖ 𝑆) ≠ ∅) | ||
Theorem | clsss2 20686 | If a subset is included in a closed set, so is the subset's closure. (Contributed by NM, 22-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐶 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝐶) → ((cls‘𝐽)‘𝑆) ⊆ 𝐶) | ||
Theorem | elcls 20687* | Membership in a closure. Theorem 6.5(a) of [Munkres] p. 95. (Contributed by NM, 22-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅))) | ||
Theorem | elcls2 20688* | Membership in a closure. (Contributed by NM, 5-Mar-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)))) | ||
Theorem | clsndisj 20689 | Any open set containing a point that belongs to the closure of a subset intersects the subset. One direction of Theorem 6.5(a) of [Munkres] p. 95. (Contributed by NM, 26-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈)) → (𝑈 ∩ 𝑆) ≠ ∅) | ||
Theorem | ntrcls0 20690 | 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 20691* | Two ways to say that a subset has an empty interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (((int‘𝐽)‘𝑆) = ∅ ↔ ∀𝑥 ∈ 𝐽 (𝑥 ⊆ 𝑆 → 𝑥 = ∅))) | ||
Theorem | cldmre 20692 | The closed sets of a topology comprise a Moore system on the points of the topology. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (Clsd‘𝐽) ∈ (Moore‘𝑋)) | ||
Theorem | mrccls 20693 | Moore closure generalizes closure in a topology. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘(Clsd‘𝐽)) ⇒ ⊢ (𝐽 ∈ Top → (cls‘𝐽) = 𝐹) | ||
Theorem | cls0 20694 | The closure of the empty set. (Contributed by NM, 2-Oct-2007.) |
⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘∅) = ∅) | ||
Theorem | ntr0 20695 | The interior of the empty set. (Contributed by NM, 2-Oct-2007.) |
⊢ (𝐽 ∈ Top → ((int‘𝐽)‘∅) = ∅) | ||
Theorem | isopn3i 20696 | An open subset equals its own interior. (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → ((int‘𝐽)‘𝑆) = 𝑆) | ||
Theorem | elcls3 20697* | Membership in a closure in terms of the members of a basis. Theorem 6.5(b) of [Munkres] p. 95. (Contributed by NM, 26-Feb-2007.) (Revised by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝜑 → 𝐽 = (topGen‘𝐵)) & ⊢ (𝜑 → 𝑋 = ∪ 𝐽) & ⊢ (𝜑 → 𝐵 ∈ TopBases) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅))) | ||
Theorem | opncldf1 20698* | A bijection useful for converting statements about open sets to statements about closed sets and vice versa. (Contributed by Jeff Hankins, 27-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐹 = (𝑢 ∈ 𝐽 ↦ (𝑋 ∖ 𝑢)) ⇒ ⊢ (𝐽 ∈ Top → (𝐹:𝐽–1-1-onto→(Clsd‘𝐽) ∧ ◡𝐹 = (𝑥 ∈ (Clsd‘𝐽) ↦ (𝑋 ∖ 𝑥)))) | ||
Theorem | opncldf2 20699* | The values of the open-closed bijection. (Contributed by Jeff Hankins, 27-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐹 = (𝑢 ∈ 𝐽 ↦ (𝑋 ∖ 𝑢)) ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → (𝐹‘𝐴) = (𝑋 ∖ 𝐴)) | ||
Theorem | opncldf3 20700* | The values of the converse/inverse of the open-closed bijection. (Contributed by Jeff Hankins, 27-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐹 = (𝑢 ∈ 𝐽 ↦ (𝑋 ∖ 𝑢)) ⇒ ⊢ (𝐵 ∈ (Clsd‘𝐽) → (◡𝐹‘𝐵) = (𝑋 ∖ 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |