Home | Metamath
Proof Explorer Theorem List (p. 216 of 449) | < 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tg2 21501* | Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.) |
⊢ ((𝐴 ∈ (topGen‘𝐵) ∧ 𝐶 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴)) | ||
Theorem | bastg 21502 | 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 21503 | 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 21504 | Subset relation for generated topologies. (Contributed by NM, 7-May-2007.) |
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶) → (topGen‘𝐵) ⊆ (topGen‘𝐶)) | ||
Theorem | tgcl 21505 | Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.) |
⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top) | ||
Theorem | tgclb 21506 | The property tgcl 21505 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 21507 | A basis generates a topology on ∪ 𝐵. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ (TopOn‘∪ 𝐵)) | ||
Theorem | topbas 21508 | A topology is its own basis. (Contributed by NM, 17-Jul-2006.) |
⊢ (𝐽 ∈ Top → 𝐽 ∈ TopBases) | ||
Theorem | tgtop 21509 | A topology is its own basis. (Contributed by NM, 18-Jul-2006.) |
⊢ (𝐽 ∈ Top → (topGen‘𝐽) = 𝐽) | ||
Theorem | eltop 21510 | Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.) |
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ 𝐴 ⊆ ∪ (𝐽 ∩ 𝒫 𝐴))) | ||
Theorem | eltop2 21511* | Membership in a topology. (Contributed by NM, 19-Jul-2006.) |
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴))) | ||
Theorem | eltop3 21512* | Membership in a topology. (Contributed by NM, 19-Jul-2006.) |
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∃𝑥(𝑥 ⊆ 𝐽 ∧ 𝐴 = ∪ 𝑥))) | ||
Theorem | fibas 21513 | A collection of finite intersections is a basis. The initial set is a subbasis for the topology. (Contributed by Jeff Hankins, 25-Aug-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ (fi‘𝐴) ∈ TopBases | ||
Theorem | tgdom 21514 | 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 21515* | 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 21516 | The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.) |
⊢ (𝐵 ∈ 𝑉 → (topGen‘(topGen‘𝐵)) = (topGen‘𝐵)) | ||
Theorem | bastop 21517 | Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.) |
⊢ (𝐵 ∈ TopBases → (𝐵 ∈ Top ↔ (topGen‘𝐵) = 𝐵)) | ||
Theorem | tgtop11 21518 | The topology generation function is one-to-one when applied to completed topologies. (Contributed by NM, 18-Jul-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ (topGen‘𝐽) = (topGen‘𝐾)) → 𝐽 = 𝐾) | ||
Theorem | 0top 21519 | The singleton of the empty set is the only topology possible for an empty underlying set. (Contributed by NM, 9-Sep-2006.) |
⊢ (𝐽 ∈ Top → (∪ 𝐽 = ∅ ↔ 𝐽 = {∅})) | ||
Theorem | en1top 21520 | {∅} is the only topology with one element. (Contributed by FL, 18-Aug-2008.) |
⊢ (𝐽 ∈ Top → (𝐽 ≈ 1o ↔ 𝐽 = {∅})) | ||
Theorem | en2top 21521 | If a topology has two elements, it is the indiscrete topology. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ≈ 2o ↔ (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅))) | ||
Theorem | tgss3 21522 | 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 21523* | 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 21524 | 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 21525* | 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 21526 | 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 21527 | 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 21528 | 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 21529* | 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 21530* | A version of bastop1 21529 that doesn't have 𝐵 ⊆ 𝐽 in the antecedent. (Contributed by NM, 3-Feb-2008.) |
⊢ (𝐽 ∈ Top → ((topGen‘𝐵) = 𝐽 ↔ (𝐵 ⊆ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)))) | ||
Theorem | distop 21531 | 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 21532 | The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 7470; an alternate proof uses indiscrete topologies (see indistop 21538) and the analogue of pwnex 7470 with pairs {∅, 𝑥} instead of power sets 𝒫 𝑥 (that analogue is also a consequence of abnex 7468). (Contributed by BJ, 2-May-2021.) |
⊢ Top ∉ V | ||
Theorem | distopon 21533 | The discrete topology on a set 𝐴, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴)) | ||
Theorem | sn0topon 21534 | The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ {∅} ∈ (TopOn‘∅) | ||
Theorem | sn0top 21535 | 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 21536 | A lemma to eliminate some sethood hypotheses when dealing with the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ {∅, ( I ‘𝐴)} = {∅, 𝐴} | ||
Theorem | indistopon 21537 | The indiscrete topology on a set 𝐴. Part of Example 2 in [Munkres] p. 77. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐴 ∈ 𝑉 → {∅, 𝐴} ∈ (TopOn‘𝐴)) | ||
Theorem | indistop 21538 | 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 21539 | The base set of the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ ( I ‘𝐴) = ∪ {∅, 𝐴} | ||
Theorem | fctop 21540* | 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 21541* | The finite complement topology on a set 𝐴. Example 3 in [Munkres] p. 77. (This version of fctop 21540 requires the Axiom of Infinity.) (Contributed by FL, 20-Aug-2006.) |
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≺ ω ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴)) | ||
Theorem | cctop 21542* | 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 21543* | The particular point topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴)) | ||
Theorem | pptbas 21544* | 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 21545* | The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 → 𝑥 = 𝐴)} ∈ (TopOn‘𝐴)) | ||
Theorem | indistpsx 21546 | The indiscrete topology on a set 𝐴 expressed as a topological space, using explicit structure component references. Compare with indistps 21547 and indistps2 21548. The advantage of this version is that the actual function for the structure is evident, and df-ndx 16474 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 16477 and df-tset 16572 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 21547 instead. (New usage is discouraged.) (Contributed by FL, 19-Jul-2006.) |
⊢ 𝐴 ∈ V & ⊢ 𝐾 = {〈1, 𝐴〉, 〈9, {∅, 𝐴}〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | indistps 21547 | The indiscrete topology on a set 𝐴 expressed as a topological space, using implicit structure indices. The advantage of this version over indistpsx 21546 is that it is independent of the indices of the component definitions df-base 16477 and df-tset 16572, and if they are changed in the future, this theorem will not be affected. The advantage over indistps2 21548 is that it is easy to eliminate the hypotheses with eqid 2818 and vtoclg 3565 to result in a closed theorem. Theorems indistpsALT 21549 and indistps2ALT 21550 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 21548 | The indiscrete topology on a set 𝐴 expressed as a topological space, using direct component assignments. Compare with indistps 21547. The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT 21549 and indistps2ALT 21550 show that the two forms can be derived from each other. (Contributed by NM, 24-Oct-2012.) |
⊢ (Base‘𝐾) = 𝐴 & ⊢ (TopOpen‘𝐾) = {∅, 𝐴} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | indistpsALT 21549 | The indiscrete topology on a set 𝐴 expressed as a topological space. Here we show how to derive the structural version indistps 21547 from the direct component assignment version indistps2 21548. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), {∅, 𝐴}〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | indistps2ALT 21550 | 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 21548 from the structural version indistps 21547. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (Base‘𝐾) = 𝐴 & ⊢ (TopOpen‘𝐾) = {∅, 𝐴} ⇒ ⊢ 𝐾 ∈ TopSp | ||
Theorem | distps 21551 | 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 21552 | Extend class notation with the set of closed sets of a topology. |
class Clsd | ||
Syntax | cnt 21553 | Extend class notation with interior of a subset of a topology base set. |
class int | ||
Syntax | ccl 21554 | Extend class notation with closure of a subset of a topology base set. |
class cls | ||
Definition | df-cld 21555* | 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 21556* | Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 21572. (Contributed by NM, 10-Sep-2006.) |
⊢ int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥))) | ||
Definition | df-cls 21557* | Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 21573. (Contributed by NM, 3-Oct-2006.) |
⊢ cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦})) | ||
Theorem | fncld 21558 | The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ Clsd Fn Top | ||
Theorem | cldval 21559* | 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 21560* | 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 21561* | 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 21562 | Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (𝐶 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) | ||
Theorem | iscld 21563 | 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 21564 | 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 21565 | 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 21566 | The set of closed sets is contained in the powerset of the base. (Contributed by Mario Carneiro, 6-Jan-2014.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (Clsd‘𝐽) ⊆ 𝒫 𝑋 | ||
Theorem | cldopn 21567 | 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 21568 | 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 21569 | The complement of an open set is closed. (Contributed by NM, 6-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → (𝑋 ∖ 𝑆) ∈ (Clsd‘𝐽)) | ||
Theorem | difopn 21570 | The difference of a closed set with an open set is open. (Contributed by Mario Carneiro, 6-Jan-2014.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ (Clsd‘𝐽)) → (𝐴 ∖ 𝐵) ∈ 𝐽) | ||
Theorem | topcld 21571 | 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 21572 | 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 21573* | 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 21574 | 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 21575* | 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 21576 | The intersection of a set of closed sets is closed. (Contributed by NM, 5-Oct-2006.) |
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ (Clsd‘𝐽)) → ∩ 𝐴 ∈ (Clsd‘𝐽)) | ||
Theorem | uncld 21577 | 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 21578 | A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007.) |
⊢ (𝑆 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘𝑆) = 𝑆) | ||
Theorem | incld 21579 | 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 21580* | An indexed relative intersection of closed sets is closed. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → (𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵) ∈ (Clsd‘𝐽)) | ||
Theorem | iuncld 21581* | A finite indexed union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) | ||
Theorem | unicld 21582 | A finite union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ (Clsd‘𝐽)) → ∪ 𝐴 ∈ (Clsd‘𝐽)) | ||
Theorem | clscld 21583 | The closure of a subset of a topology's underlying set is closed. (Contributed by NM, 4-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽)) | ||
Theorem | clsf 21584 | 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 21585 | 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 21586 | Express closure in terms of interior. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = (𝑋 ∖ ((int‘𝐽)‘(𝑋 ∖ 𝑆)))) | ||
Theorem | ntrval2 21587 | Interior expressed in terms of closure. (Contributed by NM, 1-Oct-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) = (𝑋 ∖ ((cls‘𝐽)‘(𝑋 ∖ 𝑆)))) | ||
Theorem | ntrdif 21588 | 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 21589 | A closure of a complement is the complement of the interior. (Contributed by Jeff Hankins, 31-Aug-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘(𝑋 ∖ 𝐴)) = (𝑋 ∖ ((int‘𝐽)‘𝐴))) | ||
Theorem | clsss 21590 | Subset relationship for closure. (Contributed by NM, 10-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((cls‘𝐽)‘𝑇) ⊆ ((cls‘𝐽)‘𝑆)) | ||
Theorem | ntrss 21591 | Subset relationship for interior. (Contributed by NM, 3-Oct-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((int‘𝐽)‘𝑇) ⊆ ((int‘𝐽)‘𝑆)) | ||
Theorem | sscls 21592 | A subset of a topology's underlying set is included in its closure. (Contributed by NM, 22-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆)) | ||
Theorem | ntrss2 21593 | A subset includes its interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑆) | ||
Theorem | ssntr 21594 | 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 21595 | The closure of a subset of a topological space is included in the space. (Contributed by NM, 26-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋) | ||
Theorem | ntrss3 21596 | The interior of a subset of a topological space is included in the space. (Contributed by NM, 1-Oct-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑋) | ||
Theorem | ntrin 21597 | 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 21598 | The complement of a closure is open. (Contributed by NM, 11-Sep-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∈ 𝐽) | ||
Theorem | cmntrcld 21599 | 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 21600 | A subset is closed iff it equals its own closure. (Contributed by NM, 2-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((cls‘𝐽)‘𝑆) = 𝑆)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |