Home | Metamath
Proof Explorer Theorem List (p. 217 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cmntrcld 21601 | 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 21602 | A subset is closed iff it equals its own closure. (Contributed by NM, 2-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((cls‘𝐽)‘𝑆) = 𝑆)) | ||
Theorem | iscld4 21603 | A subset is closed iff it contains its own closure. (Contributed by NM, 31-Jan-2008.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((cls‘𝐽)‘𝑆) ⊆ 𝑆)) | ||
Theorem | isopn3 21604 | 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 21605 | The closure operation is idempotent. (Contributed by NM, 2-Oct-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘((cls‘𝐽)‘𝑆)) = ((cls‘𝐽)‘𝑆)) | ||
Theorem | ntridm 21606 | The interior operation is idempotent. (Contributed by NM, 2-Oct-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘((int‘𝐽)‘𝑆)) = ((int‘𝐽)‘𝑆)) | ||
Theorem | clstop 21607 | 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 21608 | The interior of a topology's underlying set is the entire set. (Contributed by NM, 12-Sep-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → ((int‘𝐽)‘𝑋) = 𝑋) | ||
Theorem | 0ntr 21609 | A subset with an empty interior cannot cover a whole (nonempty) topology. (Contributed by NM, 12-Sep-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝑋 ≠ ∅) ∧ (𝑆 ⊆ 𝑋 ∧ ((int‘𝐽)‘𝑆) = ∅)) → (𝑋 ∖ 𝑆) ≠ ∅) | ||
Theorem | clsss2 21610 | 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 21611* | Membership in a closure. Theorem 6.5(a) of [Munkres] p. 95. (Contributed by NM, 22-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅))) | ||
Theorem | elcls2 21612* | Membership in a closure. (Contributed by NM, 5-Mar-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)))) | ||
Theorem | clsndisj 21613 | 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 21614 | 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 21615* | 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 21616 | 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 21617 | Moore closure generalizes closure in a topology. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘(Clsd‘𝐽)) ⇒ ⊢ (𝐽 ∈ Top → (cls‘𝐽) = 𝐹) | ||
Theorem | cls0 21618 | The closure of the empty set. (Contributed by NM, 2-Oct-2007.) (Proof shortened by Jim Kingdon, 12-Mar-2023.) |
⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘∅) = ∅) | ||
Theorem | ntr0 21619 | The interior of the empty set. (Contributed by NM, 2-Oct-2007.) |
⊢ (𝐽 ∈ Top → ((int‘𝐽)‘∅) = ∅) | ||
Theorem | isopn3i 21620 | An open subset equals its own interior. (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → ((int‘𝐽)‘𝑆) = 𝑆) | ||
Theorem | elcls3 21621* | 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 21622* | 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 21623* | 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 21624* | 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 21625* | 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 21626* | 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 21627 | 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 21628 | The closed sets of the topology {∅}. (Contributed by FL, 5-Jan-2009.) |
⊢ (Clsd‘{∅}) = {∅} | ||
Theorem | indiscld 21629 | The closed sets of an indiscrete topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ (Clsd‘{∅, 𝐴}) = {∅, 𝐴} | ||
Theorem | mretopd 21630* | 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‘𝐽))) | ||
Theorem | toponmre 21631 | The topologies over a given base set form a Moore collection: the intersection of any family of them is a topology, including the empty (relative) intersection which gives the discrete topology distop 21533. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ (𝐵 ∈ 𝑉 → (TopOn‘𝐵) ∈ (Moore‘𝒫 𝐵)) | ||
Theorem | cldmreon 21632 | The closed sets of a topology over a set are a Moore collection over the same set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝐵) → (Clsd‘𝐽) ∈ (Moore‘𝐵)) | ||
Theorem | iscldtop 21633* | A family is the closed sets of a topology iff it is a Moore collection and closed under finite union. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐾 ∈ (Clsd “ (TopOn‘𝐵)) ↔ (𝐾 ∈ (Moore‘𝐵) ∧ ∅ ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾)) | ||
Theorem | mreclatdemoBAD 21634 | The closed subspaces of a topology-bearing module form a complete lattice. Demonstration for mreclatBAD 17787. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 7103 update): This proof uses the old df-clat 17708 and references the required instance of mreclatBAD 17787 as a hypothesis. When mreclatBAD 17787 is corrected to become mreclat, delete this theorem and uncomment the mreclatdemo below. |
⊢ (((LSubSp‘𝑊) ∩ (Clsd‘(TopOpen‘𝑊))) ∈ (Moore‘∪ (TopOpen‘𝑊)) → (toInc‘((LSubSp‘𝑊) ∩ (Clsd‘(TopOpen‘𝑊)))) ∈ CLat) ⇒ ⊢ (𝑊 ∈ (TopSp ∩ LMod) → (toInc‘((LSubSp‘𝑊) ∩ (Clsd‘(TopOpen‘𝑊)))) ∈ CLat) | ||
Syntax | cnei 21635 | Extend class notation with neighborhood relation for topologies. |
class nei | ||
Definition | df-nei 21636* | Define a function on topologies whose value is a map from a subset to its neighborhoods. (Contributed by NM, 11-Feb-2007.) |
⊢ nei = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∈ 𝒫 ∪ 𝑗 ∣ ∃𝑔 ∈ 𝑗 (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)})) | ||
Theorem | neifval 21637* | 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.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (nei‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ {𝑣 ∈ 𝒫 𝑋 ∣ ∃𝑔 ∈ 𝐽 (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣)})) | ||
Theorem | neif 21638 | 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.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (nei‘𝐽) Fn 𝒫 𝑋) | ||
Theorem | neiss2 21639 | 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.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑋) | ||
Theorem | neival 21640* | 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.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((nei‘𝐽)‘𝑆) = {𝑣 ∈ 𝒫 𝑋 ∣ ∃𝑔 ∈ 𝐽 (𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣)}) | ||
Theorem | isnei 21641* | The predicate "the class 𝑁 is a neighborhood of 𝑆". (Contributed by FL, 25-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘𝑆) ↔ (𝑁 ⊆ 𝑋 ∧ ∃𝑔 ∈ 𝐽 (𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁)))) | ||
Theorem | neiint 21642 | An intuitive definition of a neighborhood in terms of interior. (Contributed by Szymon Jaroszewicz, 18-Dec-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘𝑆) ↔ 𝑆 ⊆ ((int‘𝐽)‘𝑁))) | ||
Theorem | isneip 21643* | The predicate "the class 𝑁 is a neighborhood of point 𝑃". (Contributed by NM, 26-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ 𝑋 ∧ ∃𝑔 ∈ 𝐽 (𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁)))) | ||
Theorem | neii1 21644 | A neighborhood is included in the topology's base set. (Contributed by NM, 12-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑁 ⊆ 𝑋) | ||
Theorem | neisspw 21645 | The neighborhoods of any set are subsets of the base set. (Contributed by Stefan O'Rear, 6-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘𝑆) ⊆ 𝒫 𝑋) | ||
Theorem | neii2 21646* | Property of a neighborhood. (Contributed by NM, 12-Feb-2007.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → ∃𝑔 ∈ 𝐽 (𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁)) | ||
Theorem | neiss 21647 | 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.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑅 ⊆ 𝑆) → 𝑁 ∈ ((nei‘𝐽)‘𝑅)) | ||
Theorem | ssnei 21648 | A set is included in any of its neighborhoods. Generalization to subsets of elnei 21649. (Contributed by FL, 16-Nov-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑁) | ||
Theorem | elnei 21649 | A point belongs to any of its neighborhoods. Property Viii of [BourbakiTop1] p. I.3. (Contributed by FL, 28-Sep-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝐴 ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑃 ∈ 𝑁) | ||
Theorem | 0nnei 21650 | The empty set is not a neighborhood of a nonempty set. (Contributed by FL, 18-Sep-2007.) |
⊢ ((𝐽 ∈ Top ∧ 𝑆 ≠ ∅) → ¬ ∅ ∈ ((nei‘𝐽)‘𝑆)) | ||
Theorem | neips 21651* | A neighborhood of a set is a neighborhood of every point in the set. Proposition 1 of [BourbakiTop1] p. I.2. (Contributed by FL, 16-Nov-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (𝑁 ∈ ((nei‘𝐽)‘𝑆) ↔ ∀𝑝 ∈ 𝑆 𝑁 ∈ ((nei‘𝐽)‘{𝑝}))) | ||
Theorem | opnneissb 21652 | An open set is a neighborhood of any of its subsets. (Contributed by FL, 2-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋) → (𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ((nei‘𝐽)‘𝑆))) | ||
Theorem | opnssneib 21653 | Any superset of an open set is a neighborhood of it. (Contributed by NM, 14-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ∧ 𝑁 ⊆ 𝑋) → (𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ((nei‘𝐽)‘𝑆))) | ||
Theorem | ssnei2 21654 | Any subset 𝑀 of 𝑋 containing a neighborhood 𝑁 of a set 𝑆 is a neighborhood of this set. Generalization to subsets of Property Vi of [BourbakiTop1] p. I.3. (Contributed by FL, 2-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) ∧ (𝑁 ⊆ 𝑀 ∧ 𝑀 ⊆ 𝑋)) → 𝑀 ∈ ((nei‘𝐽)‘𝑆)) | ||
Theorem | neindisj 21655 | Any neighborhood of an element in the closure of a subset intersects the subset. Part of proof of Theorem 6.6 of [Munkres] p. 97. (Contributed by NM, 26-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑃 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃}))) → (𝑁 ∩ 𝑆) ≠ ∅) | ||
Theorem | opnneiss 21656 | An open set is a neighborhood of any of its subsets. (Contributed by NM, 13-Feb-2007.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘𝑆)) | ||
Theorem | opnneip 21657 | An open set is a neighborhood of any of its members. (Contributed by NM, 8-Mar-2007.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑃 ∈ 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) | ||
Theorem | opnnei 21658* | A set is open iff it is a neighborhood of all of its points. (Contributed by Jeff Hankins, 15-Sep-2009.) |
⊢ (𝐽 ∈ Top → (𝑆 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}))) | ||
Theorem | tpnei 21659 | The underlying set of a topology is a neighborhood of any of its subsets. Special case of opnneiss 21656. (Contributed by FL, 2-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (𝑆 ⊆ 𝑋 ↔ 𝑋 ∈ ((nei‘𝐽)‘𝑆))) | ||
Theorem | neiuni 21660 | The union of the neighborhoods of a set equals the topology's underlying set. (Contributed by FL, 18-Sep-2007.) (Revised by Mario Carneiro, 9-Apr-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑋 = ∪ ((nei‘𝐽)‘𝑆)) | ||
Theorem | neindisj2 21661* | A point 𝑃 belongs to the closure of a set 𝑆 iff every neighborhood of 𝑃 meets 𝑆. (Contributed by FL, 15-Sep-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝑃})(𝑛 ∩ 𝑆) ≠ ∅)) | ||
Theorem | topssnei 21662 | A finer topology has more neighborhoods. (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌) ∧ 𝐽 ⊆ 𝐾) → ((nei‘𝐽)‘𝑆) ⊆ ((nei‘𝐾)‘𝑆)) | ||
Theorem | innei 21663 | The intersection of two neighborhoods of a set is also a neighborhood of the set. Generalization to subsets of Property Vii of [BourbakiTop1] p. I.3 for binary intersections. (Contributed by FL, 28-Sep-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑀 ∈ ((nei‘𝐽)‘𝑆)) → (𝑁 ∩ 𝑀) ∈ ((nei‘𝐽)‘𝑆)) | ||
Theorem | opnneiid 21664 | Only an open set is a neighborhood of itself. (Contributed by FL, 2-Oct-2006.) |
⊢ (𝐽 ∈ Top → (𝑁 ∈ ((nei‘𝐽)‘𝑁) ↔ 𝑁 ∈ 𝐽)) | ||
Theorem | neissex 21665* | For any neighborhood 𝑁 of 𝑆, there is a neighborhood 𝑥 of 𝑆 such that 𝑁 is a neighborhood of all subsets of 𝑥. Generalization to subsets of Property Viv of [BourbakiTop1] p. I.3. (Contributed by FL, 2-Oct-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → ∃𝑥 ∈ ((nei‘𝐽)‘𝑆)∀𝑦(𝑦 ⊆ 𝑥 → 𝑁 ∈ ((nei‘𝐽)‘𝑦))) | ||
Theorem | 0nei 21666 | The empty set is a neighborhood of itself. (Contributed by FL, 10-Dec-2006.) |
⊢ (𝐽 ∈ Top → ∅ ∈ ((nei‘𝐽)‘∅)) | ||
Theorem | neipeltop 21667* | Lemma for neiptopreu 21671. (Contributed by Thierry Arnoux, 6-Jan-2018.) |
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} ⇒ ⊢ (𝐶 ∈ 𝐽 ↔ (𝐶 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝐶 𝐶 ∈ (𝑁‘𝑝))) | ||
Theorem | neiptopuni 21668* | Lemma for neiptopreu 21671. (Contributed by Thierry Arnoux, 6-Jan-2018.) |
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} & ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋) & ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) ⇒ ⊢ (𝜑 → 𝑋 = ∪ 𝐽) | ||
Theorem | neiptoptop 21669* | Lemma for neiptopreu 21671. (Contributed by Thierry Arnoux, 7-Jan-2018.) |
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} & ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋) & ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) ⇒ ⊢ (𝜑 → 𝐽 ∈ Top) | ||
Theorem | neiptopnei 21670* | Lemma for neiptopreu 21671. (Contributed by Thierry Arnoux, 7-Jan-2018.) |
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} & ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋) & ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) ⇒ ⊢ (𝜑 → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝}))) | ||
Theorem | neiptopreu 21671* | If, to each element 𝑃 of a set 𝑋, we associate a set (𝑁‘𝑃) fulfilling Properties Vi, Vii, Viii and Property Viv of [BourbakiTop1] p. I.2. , corresponding to ssnei 21648, innei 21663, elnei 21649 and neissex 21665, then there is a unique topology 𝑗 such that for any point 𝑝, (𝑁‘𝑝) is the set of neighborhoods of 𝑝. Proposition 2 of [BourbakiTop1] p. I.3. This can be used to build a topology from a set of neighborhoods. Note that innei 21663 uses binary intersections whereas Property Vii mentions finite intersections (which includes the empty intersection of subsets of 𝑋, which is equal to 𝑋), so we add the hypothesis that 𝑋 is a neighborhood of all points. TODO: when df-fi 8864 includes the empty intersection, remove that extra hypothesis. (Contributed by Thierry Arnoux, 6-Jan-2018.) |
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} & ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋) & ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) ⇒ ⊢ (𝜑 → ∃!𝑗 ∈ (TopOn‘𝑋)𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) | ||
Syntax | clp 21672 | Extend class notation with the limit point function for topologies. |
class limPt | ||
Syntax | cperf 21673 | Extend class notation with the class of all perfect spaces. |
class Perf | ||
Definition | df-lp 21674* | Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval 21677. (Contributed by NM, 10-Feb-2007.) |
⊢ limPt = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))})) | ||
Definition | df-perf 21675 | Define the class of all perfect spaces. A perfect space is one for which every point in the set is a limit point of the whole space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ Perf = {𝑗 ∈ Top ∣ ((limPt‘𝑗)‘∪ 𝑗) = ∪ 𝑗} | ||
Theorem | lpfval 21676* | The limit point function on the subsets of a topology's base set. (Contributed by NM, 10-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (limPt‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝐽)‘(𝑥 ∖ {𝑦}))})) | ||
Theorem | lpval 21677* | The set of limit points of a subset of the base set of a topology. Alternate definition of limit point in [Munkres] p. 97. (Contributed by NM, 10-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑆) = {𝑥 ∣ 𝑥 ∈ ((cls‘𝐽)‘(𝑆 ∖ {𝑥}))}) | ||
Theorem | islp 21678 | The predicate "the class 𝑃 is a limit point of 𝑆". (Contributed by NM, 10-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑆) ↔ 𝑃 ∈ ((cls‘𝐽)‘(𝑆 ∖ {𝑃})))) | ||
Theorem | lpsscls 21679 | The limit points of a subset are included in the subset's closure. (Contributed by NM, 26-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑆) ⊆ ((cls‘𝐽)‘𝑆)) | ||
Theorem | lpss 21680 | The limit points of a subset are included in the base set. (Contributed by NM, 9-Nov-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑆) ⊆ 𝑋) | ||
Theorem | lpdifsn 21681 | 𝑃 is a limit point of 𝑆 iff it is a limit point of 𝑆 ∖ {𝑃}. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑆) ↔ 𝑃 ∈ ((limPt‘𝐽)‘(𝑆 ∖ {𝑃})))) | ||
Theorem | lpss3 21682 | Subset relationship for limit points. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((limPt‘𝐽)‘𝑇) ⊆ ((limPt‘𝐽)‘𝑆)) | ||
Theorem | islp2 21683* | The predicate "𝑃 is a limit point of 𝑆 " in terms of neighborhoods. Definition of limit point in [Munkres] p. 97. Although Munkres uses open neighborhoods, it also works for our more general neighborhoods. (Contributed by NM, 26-Feb-2007.) (Proof shortened by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑆) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝑃})(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅)) | ||
Theorem | islp3 21684* | The predicate "𝑃 is a limit point of 𝑆 " in terms of open sets. see islp2 21683, elcls 21611, islp 21678. (Contributed by FL, 31-Jul-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ (𝑆 ∖ {𝑃})) ≠ ∅))) | ||
Theorem | maxlp 21685 | A point is a limit point of the whole space iff the singleton of the point is not open. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (𝑃 ∈ ((limPt‘𝐽)‘𝑋) ↔ (𝑃 ∈ 𝑋 ∧ ¬ {𝑃} ∈ 𝐽))) | ||
Theorem | clslp 21686 | The closure of a subset of a topological space is the subset together with its limit points. Theorem 6.6 of [Munkres] p. 97. (Contributed by NM, 26-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = (𝑆 ∪ ((limPt‘𝐽)‘𝑆))) | ||
Theorem | islpi 21687 | A point belonging to a set's closure but not the set itself is a limit point. (Contributed by NM, 8-Nov-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑃 ∈ ((cls‘𝐽)‘𝑆) ∧ ¬ 𝑃 ∈ 𝑆)) → 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) | ||
Theorem | cldlp 21688 | A subset of a topological space is closed iff it contains all its limit points. Corollary 6.7 of [Munkres] p. 97. (Contributed by NM, 26-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑆) ⊆ 𝑆)) | ||
Theorem | isperf 21689 | Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Perf ↔ (𝐽 ∈ Top ∧ ((limPt‘𝐽)‘𝑋) = 𝑋)) | ||
Theorem | isperf2 21690 | Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Perf ↔ (𝐽 ∈ Top ∧ 𝑋 ⊆ ((limPt‘𝐽)‘𝑋))) | ||
Theorem | isperf3 21691* | A perfect space is a topology which has no open singletons. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Perf ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ¬ {𝑥} ∈ 𝐽)) | ||
Theorem | perflp 21692 | The limit points of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Perf → ((limPt‘𝐽)‘𝑋) = 𝑋) | ||
Theorem | perfi 21693 | Property of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Perf ∧ 𝑃 ∈ 𝑋) → ¬ {𝑃} ∈ 𝐽) | ||
Theorem | perftop 21694 | A perfect space is a topology. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ (𝐽 ∈ Perf → 𝐽 ∈ Top) | ||
Theorem | restrcl 21695 | Reverse closure for the subspace topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ ((𝐽 ↾t 𝐴) ∈ Top → (𝐽 ∈ V ∧ 𝐴 ∈ V)) | ||
Theorem | restbas 21696 | A subspace topology basis is a basis. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ (𝐵 ∈ TopBases → (𝐵 ↾t 𝐴) ∈ TopBases) | ||
Theorem | tgrest 21697 | A subspace can be generated by restricted sets from a basis for the original topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Proof shortened by Mario Carneiro, 30-Aug-2015.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (topGen‘(𝐵 ↾t 𝐴)) = ((topGen‘𝐵) ↾t 𝐴)) | ||
Theorem | resttop 21698 | A subspace topology is a topology. Definition of subspace topology in [Munkres] p. 89. 𝐴 is normally a subset of the base set of 𝐽. (Contributed by FL, 15-Apr-2007.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ Top) | ||
Theorem | resttopon 21699 | A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴)) | ||
Theorem | restuni 21700 | The underlying set of a subspace topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |