| Metamath
Proof Explorer Theorem List (p. 231 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | bastop2 23001* | A version of bastop1 23000 that doesn't have 𝐵 ⊆ 𝐽 in the antecedent. (Contributed by NM, 3-Feb-2008.) |
| ⊢ (𝐽 ∈ Top → ((topGen‘𝐵) = 𝐽 ↔ (𝐵 ⊆ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)))) | ||
| Theorem | distop 23002 | 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 23003 | The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 7779; an alternate proof uses indiscrete topologies (see indistop 23009) and the analogue of pwnex 7779 with pairs {∅, 𝑥} instead of power sets 𝒫 𝑥 (that analogue is also a consequence of abnex 7777). (Contributed by BJ, 2-May-2021.) |
| ⊢ Top ∉ V | ||
| Theorem | distopon 23004 | The discrete topology on a set 𝐴, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴)) | ||
| Theorem | sn0topon 23005 | The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ {∅} ∈ (TopOn‘∅) | ||
| Theorem | sn0top 23006 | 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 23007 | A lemma to eliminate some sethood hypotheses when dealing with the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| ⊢ {∅, ( I ‘𝐴)} = {∅, 𝐴} | ||
| Theorem | indistopon 23008 | The indiscrete topology on a set 𝐴. Part of Example 2 in [Munkres] p. 77. (Contributed by Mario Carneiro, 13-Aug-2015.) |
| ⊢ (𝐴 ∈ 𝑉 → {∅, 𝐴} ∈ (TopOn‘𝐴)) | ||
| Theorem | indistop 23009 | 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 23010 | The base set of the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| ⊢ ( I ‘𝐴) = ∪ {∅, 𝐴} | ||
| Theorem | fctop 23011* | 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 23012* | The finite complement topology on a set 𝐴. Example 3 in [Munkres] p. 77. (This version of fctop 23011 requires the Axiom of Infinity.) (Contributed by FL, 20-Aug-2006.) |
| ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≺ ω ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴)) | ||
| Theorem | cctop 23013* | 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 23014* | The particular point topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴)) | ||
| Theorem | pptbas 23015* | 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 23016* | The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 → 𝑥 = 𝐴)} ∈ (TopOn‘𝐴)) | ||
| Theorem | indistpsx 23017 | The indiscrete topology on a set 𝐴 expressed as a topological space, using explicit structure component references. Compare with indistps 23018 and indistps2 23019. The advantage of this version is that the actual function for the structure is evident, and df-ndx 17231 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 17248 and df-tset 17316 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 23018 instead. (New usage is discouraged.) (Contributed by FL, 19-Jul-2006.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐾 = {〈1, 𝐴〉, 〈9, {∅, 𝐴}〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
| Theorem | indistps 23018 | The indiscrete topology on a set 𝐴 expressed as a topological space, using implicit structure indices. The advantage of this version over indistpsx 23017 is that it is independent of the indices of the component definitions df-base 17248 and df-tset 17316, and if they are changed in the future, this theorem will not be affected. The advantage over indistps2 23019 is that it is easy to eliminate the hypotheses with eqid 2737 and vtoclg 3554 to result in a closed theorem. Theorems indistpsALT 23020 and indistps2ALT 23022 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 23019 | The indiscrete topology on a set 𝐴 expressed as a topological space, using direct component assignments. Compare with indistps 23018. The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT 23020 and indistps2ALT 23022 show that the two forms can be derived from each other. (Contributed by NM, 24-Oct-2012.) |
| ⊢ (Base‘𝐾) = 𝐴 & ⊢ (TopOpen‘𝐾) = {∅, 𝐴} ⇒ ⊢ 𝐾 ∈ TopSp | ||
| Theorem | indistpsALT 23020 | The indiscrete topology on a set 𝐴 expressed as a topological space. Here we show how to derive the structural version indistps 23018 from the direct component assignment version indistps2 23019. (Contributed by NM, 24-Oct-2012.) (Revised by AV, 31-Oct-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), {∅, 𝐴}〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
| Theorem | indistpsALTOLD 23021 | Obsolete version of indistpsALT 23020 as of 31-Oct-2024. The indiscrete topology on a set 𝐴 expressed as a topological space. Here we show how to derive the structural version indistps 23018 from the direct component assignment version indistps2 23019. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), {∅, 𝐴}〉} ⇒ ⊢ 𝐾 ∈ TopSp | ||
| Theorem | indistps2ALT 23022 | 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 23019 from the structural version indistps 23018. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (Base‘𝐾) = 𝐴 & ⊢ (TopOpen‘𝐾) = {∅, 𝐴} ⇒ ⊢ 𝐾 ∈ TopSp | ||
| Theorem | distps 23023 | 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 23024 | Extend class notation with the set of closed sets of a topology. |
| class Clsd | ||
| Syntax | cnt 23025 | Extend class notation with interior of a subset of a topology base set. |
| class int | ||
| Syntax | ccl 23026 | Extend class notation with closure of a subset of a topology base set. |
| class cls | ||
| Definition | df-cld 23027* | 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 23028* | Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 23044. (Contributed by NM, 10-Sep-2006.) |
| ⊢ int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥))) | ||
| Definition | df-cls 23029* | Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 23045. (Contributed by NM, 3-Oct-2006.) |
| ⊢ cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦})) | ||
| Theorem | fncld 23030 | The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ Clsd Fn Top | ||
| Theorem | cldval 23031* | 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 23032* | 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 23033* | 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 23034 | Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
| ⊢ (𝐶 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) | ||
| Theorem | iscld 23035 | 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 23036 | 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 23037 | 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 23038 | The set of closed sets is contained in the powerset of the base. (Contributed by Mario Carneiro, 6-Jan-2014.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (Clsd‘𝐽) ⊆ 𝒫 𝑋 | ||
| Theorem | cldopn 23039 | 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 23040 | 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 23041 | The complement of an open set is closed. (Contributed by NM, 6-Oct-2006.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → (𝑋 ∖ 𝑆) ∈ (Clsd‘𝐽)) | ||
| Theorem | difopn 23042 | The difference of a closed set with an open set is open. (Contributed by Mario Carneiro, 6-Jan-2014.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ (Clsd‘𝐽)) → (𝐴 ∖ 𝐵) ∈ 𝐽) | ||
| Theorem | topcld 23043 | 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 23044 | 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 23045* | 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 23046 | 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 23047* | 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 23048 | The intersection of a set of closed sets is closed. (Contributed by NM, 5-Oct-2006.) |
| ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ (Clsd‘𝐽)) → ∩ 𝐴 ∈ (Clsd‘𝐽)) | ||
| Theorem | uncld 23049 | 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 23050 | A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007.) |
| ⊢ (𝑆 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘𝑆) = 𝑆) | ||
| Theorem | incld 23051 | 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 23052* | An indexed relative intersection of closed sets is closed. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → (𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵) ∈ (Clsd‘𝐽)) | ||
| Theorem | iuncld 23053* | A finite indexed union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) | ||
| Theorem | unicld 23054 | A finite union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ (Clsd‘𝐽)) → ∪ 𝐴 ∈ (Clsd‘𝐽)) | ||
| Theorem | clscld 23055 | The closure of a subset of a topology's underlying set is closed. (Contributed by NM, 4-Oct-2006.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽)) | ||
| Theorem | clsf 23056 | 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 23057 | 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 23058 | Express closure in terms of interior. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = (𝑋 ∖ ((int‘𝐽)‘(𝑋 ∖ 𝑆)))) | ||
| Theorem | ntrval2 23059 | Interior expressed in terms of closure. (Contributed by NM, 1-Oct-2007.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) = (𝑋 ∖ ((cls‘𝐽)‘(𝑋 ∖ 𝑆)))) | ||
| Theorem | ntrdif 23060 | 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 23061 | A closure of a complement is the complement of the interior. (Contributed by Jeff Hankins, 31-Aug-2009.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘(𝑋 ∖ 𝐴)) = (𝑋 ∖ ((int‘𝐽)‘𝐴))) | ||
| Theorem | clsss 23062 | Subset relationship for closure. (Contributed by NM, 10-Feb-2007.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((cls‘𝐽)‘𝑇) ⊆ ((cls‘𝐽)‘𝑆)) | ||
| Theorem | ntrss 23063 | Subset relationship for interior. (Contributed by NM, 3-Oct-2007.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((int‘𝐽)‘𝑇) ⊆ ((int‘𝐽)‘𝑆)) | ||
| Theorem | sscls 23064 | A subset of a topology's underlying set is included in its closure. (Contributed by NM, 22-Feb-2007.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆)) | ||
| Theorem | ntrss2 23065 | A subset includes its interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑆) | ||
| Theorem | ssntr 23066 | 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 23067 | The closure of a subset of a topological space is included in the space. (Contributed by NM, 26-Feb-2007.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋) | ||
| Theorem | ntrss3 23068 | The interior of a subset of a topological space is included in the space. (Contributed by NM, 1-Oct-2007.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑋) | ||
| Theorem | ntrin 23069 | 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 23070 | The complement of a closure is open. (Contributed by NM, 11-Sep-2006.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∈ 𝐽) | ||
| Theorem | cmntrcld 23071 | 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 23072 | A subset is closed iff it equals its own closure. (Contributed by NM, 2-Oct-2006.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((cls‘𝐽)‘𝑆) = 𝑆)) | ||
| Theorem | iscld4 23073 | A subset is closed iff it contains its own closure. (Contributed by NM, 31-Jan-2008.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((cls‘𝐽)‘𝑆) ⊆ 𝑆)) | ||
| Theorem | isopn3 23074 | 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 23075 | The closure operation is idempotent. (Contributed by NM, 2-Oct-2007.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘((cls‘𝐽)‘𝑆)) = ((cls‘𝐽)‘𝑆)) | ||
| Theorem | ntridm 23076 | The interior operation is idempotent. (Contributed by NM, 2-Oct-2007.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘((int‘𝐽)‘𝑆)) = ((int‘𝐽)‘𝑆)) | ||
| Theorem | clstop 23077 | 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 23078 | The interior of a topology's underlying set is the entire set. (Contributed by NM, 12-Sep-2006.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → ((int‘𝐽)‘𝑋) = 𝑋) | ||
| Theorem | 0ntr 23079 | A subset with an empty interior cannot cover a whole (nonempty) topology. (Contributed by NM, 12-Sep-2006.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝑋 ≠ ∅) ∧ (𝑆 ⊆ 𝑋 ∧ ((int‘𝐽)‘𝑆) = ∅)) → (𝑋 ∖ 𝑆) ≠ ∅) | ||
| Theorem | clsss2 23080 | 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 23081* | Membership in a closure. Theorem 6.5(a) of [Munkres] p. 95. (Contributed by NM, 22-Feb-2007.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅))) | ||
| Theorem | elcls2 23082* | Membership in a closure. (Contributed by NM, 5-Mar-2007.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)))) | ||
| Theorem | clsndisj 23083 | 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 23084 | 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 23085* | 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 23086 | 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 23087 | Moore closure generalizes closure in a topology. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ 𝐹 = (mrCls‘(Clsd‘𝐽)) ⇒ ⊢ (𝐽 ∈ Top → (cls‘𝐽) = 𝐹) | ||
| Theorem | cls0 23088 | The closure of the empty set. (Contributed by NM, 2-Oct-2007.) (Proof shortened by Jim Kingdon, 12-Mar-2023.) |
| ⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘∅) = ∅) | ||
| Theorem | ntr0 23089 | The interior of the empty set. (Contributed by NM, 2-Oct-2007.) |
| ⊢ (𝐽 ∈ Top → ((int‘𝐽)‘∅) = ∅) | ||
| Theorem | isopn3i 23090 | An open subset equals its own interior. (Contributed by Mario Carneiro, 30-Dec-2016.) |
| ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → ((int‘𝐽)‘𝑆) = 𝑆) | ||
| Theorem | elcls3 23091* | 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 23092* | 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 23093* | 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 23094* | 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‘𝐽) → (◡𝐹‘𝐵) = (𝑋 ∖ 𝐵)) | ||
| Theorem | isclo 23095* | A set 𝐴 is clopen iff for every point 𝑥 in the space there is a neighborhood 𝑦 such that all the points in 𝑦 are in 𝐴 iff 𝑥 is. (Contributed by Mario Carneiro, 10-Mar-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)))) | ||
| Theorem | isclo2 23096* | A set 𝐴 is clopen iff for every point 𝑥 in the space there is a neighborhood 𝑦 of 𝑥 which is either disjoint from 𝐴 or contained in 𝐴. (Contributed by Mario Carneiro, 7-Jul-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴)))) | ||
| Theorem | discld 23097 | 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 23098 | The closed sets of the topology {∅}. (Contributed by FL, 5-Jan-2009.) |
| ⊢ (Clsd‘{∅}) = {∅} | ||
| Theorem | indiscld 23099 | The closed sets of an indiscrete topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 14-Aug-2015.) |
| ⊢ (Clsd‘{∅, 𝐴}) = {∅, 𝐴} | ||
| Theorem | mretopd 23100* | A Moore collection which is closed under finite unions called topological; such a collection is the closed sets of a canonically associated topology. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ (𝜑 → 𝑀 ∈ (Moore‘𝐵)) & ⊢ (𝜑 → ∅ ∈ 𝑀) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀) → (𝑥 ∪ 𝑦) ∈ 𝑀) & ⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ⇒ ⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ 𝑀 = (Clsd‘𝐽))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |