![]() |
Metamath
Proof Explorer Theorem List (p. 217 of 435) | < 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-28326) |
![]() (28327-29851) |
![]() (29852-43457) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | connsuba 21601* | Connectedness for a subspace. See connsub 21602. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝐽 ↾t 𝐴) ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (((𝑥 ∩ 𝐴) ≠ ∅ ∧ (𝑦 ∩ 𝐴) ≠ ∅ ∧ ((𝑥 ∩ 𝑦) ∩ 𝐴) = ∅) → ((𝑥 ∪ 𝑦) ∩ 𝐴) ≠ 𝐴))) | ||
Theorem | connsub 21602* | Two equivalent ways of saying that a subspace topology is connected. (Contributed by Jeff Hankins, 9-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (((𝑥 ∩ 𝑆) ≠ ∅ ∧ (𝑦 ∩ 𝑆) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ 𝑆)) → ¬ 𝑆 ⊆ (𝑥 ∪ 𝑦)))) | ||
Theorem | cnconn 21603 | Connectedness is respected by a continuous onto map. (Contributed by Jeff Hankins, 12-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ ((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Conn) | ||
Theorem | nconnsubb 21604 | Disconnectedness for a subspace. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → 𝑈 ∈ 𝐽) & ⊢ (𝜑 → 𝑉 ∈ 𝐽) & ⊢ (𝜑 → (𝑈 ∩ 𝐴) ≠ ∅) & ⊢ (𝜑 → (𝑉 ∩ 𝐴) ≠ ∅) & ⊢ (𝜑 → ((𝑈 ∩ 𝑉) ∩ 𝐴) = ∅) & ⊢ (𝜑 → 𝐴 ⊆ (𝑈 ∪ 𝑉)) ⇒ ⊢ (𝜑 → ¬ (𝐽 ↾t 𝐴) ∈ Conn) | ||
Theorem | connsubclo 21605 | If a clopen set meets a connected subspace, it must contain the entire subspace. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝐽 ↾t 𝐴) ∈ Conn) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) & ⊢ (𝜑 → (𝐵 ∩ 𝐴) ≠ ∅) & ⊢ (𝜑 → 𝐵 ∈ (Clsd‘𝐽)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | connima 21606 | The image of a connected set is connected. (Contributed by Mario Carneiro, 7-Jul-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝐽 ↾t 𝐴) ∈ Conn) ⇒ ⊢ (𝜑 → (𝐾 ↾t (𝐹 “ 𝐴)) ∈ Conn) | ||
Theorem | conncn 21607 | A continuous function from a connected topology with one point in a clopen set must lie entirely within the set. (Contributed by Mario Carneiro, 16-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐽 ∈ Conn) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝑈 ∈ 𝐾) & ⊢ (𝜑 → 𝑈 ∈ (Clsd‘𝐾)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶𝑈) | ||
Theorem | iunconnlem 21608* | Lemma for iunconn 21609. (Contributed by Mario Carneiro, 11-Jun-2014.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾t 𝐵) ∈ Conn) & ⊢ (𝜑 → 𝑈 ∈ 𝐽) & ⊢ (𝜑 → 𝑉 ∈ 𝐽) & ⊢ (𝜑 → (𝑉 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅) & ⊢ (𝜑 → (𝑈 ∩ 𝑉) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵)) & ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑈 ∪ 𝑉)) & ⊢ Ⅎ𝑘𝜑 ⇒ ⊢ (𝜑 → ¬ 𝑃 ∈ 𝑈) | ||
Theorem | iunconn 21609* | The indexed union of connected overlapping subspaces sharing a common point is connected. (Contributed by Mario Carneiro, 11-Jun-2014.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾t 𝐵) ∈ Conn) ⇒ ⊢ (𝜑 → (𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵) ∈ Conn) | ||
Theorem | unconn 21610 | The union of two connected overlapping subspaces is connected. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 11-Jun-2014.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ (𝐴 ∩ 𝐵) ≠ ∅) → (((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn) → (𝐽 ↾t (𝐴 ∪ 𝐵)) ∈ Conn)) | ||
Theorem | clsconn 21611 | The closure of a connected set is connected. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Conn) → (𝐽 ↾t ((cls‘𝐽)‘𝐴)) ∈ Conn) | ||
Theorem | conncompid 21612* | The connected component containing 𝐴 contains 𝐴. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑆) | ||
Theorem | conncompconn 21613* | The connected component containing 𝐴 is connected. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Conn) | ||
Theorem | conncompss 21614* | The connected component containing 𝐴 is a superset of any other connected set containing 𝐴. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⇒ ⊢ ((𝑇 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑇 ∧ (𝐽 ↾t 𝑇) ∈ Conn) → 𝑇 ⊆ 𝑆) | ||
Theorem | conncompcld 21615* | The connected component containing 𝐴 is a closed set. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → 𝑆 ∈ (Clsd‘𝐽)) | ||
Theorem | conncompclo 21616* | The connected component containing 𝐴 is a subset of any clopen set containing 𝐴. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑇 ∈ (𝐽 ∩ (Clsd‘𝐽)) ∧ 𝐴 ∈ 𝑇) → 𝑆 ⊆ 𝑇) | ||
Theorem | t1connperf 21617 | A connected T1 space is perfect, unless it is the topology of a singleton. (Contributed by Mario Carneiro, 26-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Fre ∧ 𝐽 ∈ Conn ∧ ¬ 𝑋 ≈ 1o) → 𝐽 ∈ Perf) | ||
Syntax | c1stc 21618 | Extend class definition to include the class of all first-countable topologies. |
class 1st𝜔 | ||
Syntax | c2ndc 21619 | Extend class definition to include the class of all second-countable topologies. |
class 2nd𝜔 | ||
Definition | df-1stc 21620* | Define the class of all first-countable topologies. (Contributed by Jeff Hankins, 22-Aug-2009.) |
⊢ 1st𝜔 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))} | ||
Definition | df-2ndc 21621* | Define the class of all second-countable topologies. (Contributed by Jeff Hankins, 17-Jan-2010.) |
⊢ 2nd𝜔 = {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)} | ||
Theorem | is1stc 21622* | The predicate "is a first-countable topology." This can be described as "every point has a countable local basis" - that is, every point has a countable collection of open sets containing it such that every open set containing the point has an open set from this collection as a subset. (Contributed by Jeff Hankins, 22-Aug-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ 1st𝜔 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧))))) | ||
Theorem | is1stc2 21623* | An equivalent way of saying "is a first-countable topology." (Contributed by Jeff Hankins, 22-Aug-2009.) (Revised by Mario Carneiro, 21-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ 1st𝜔 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) | ||
Theorem | 1stctop 21624 | A first-countable topology is a topology. (Contributed by Jeff Hankins, 22-Aug-2009.) |
⊢ (𝐽 ∈ 1st𝜔 → 𝐽 ∈ Top) | ||
Theorem | 1stcclb 21625* | A property of points in a first-countable topology. (Contributed by Jeff Hankins, 22-Aug-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) → ∃𝑥 ∈ 𝒫 𝐽(𝑥 ≼ ω ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑧 ∈ 𝑥 (𝐴 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)))) | ||
Theorem | 1stcfb 21626* | For any point 𝐴 in a first-countable topology, there is a function 𝑓:ℕ⟶𝐽 enumerating neighborhoods of 𝐴 which is decreasing and forms a local base. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦))) | ||
Theorem | is2ndc 21627* | The property of being second-countable. (Contributed by Jeff Hankins, 17-Jan-2010.) (Revised by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐽 ∈ 2nd𝜔 ↔ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝐽)) | ||
Theorem | 2ndctop 21628 | A second-countable topology is a topology. (Contributed by Jeff Hankins, 17-Jan-2010.) (Revised by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐽 ∈ 2nd𝜔 → 𝐽 ∈ Top) | ||
Theorem | 2ndci 21629 | A countable basis generates a second-countable topology. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐵 ∈ TopBases ∧ 𝐵 ≼ ω) → (topGen‘𝐵) ∈ 2nd𝜔) | ||
Theorem | 2ndcsb 21630* | Having a countable subbase is a sufficient condition for second-countability. (Contributed by Jeff Hankins, 17-Jan-2010.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐽 ∈ 2nd𝜔 ↔ ∃𝑥(𝑥 ≼ ω ∧ (topGen‘(fi‘𝑥)) = 𝐽)) | ||
Theorem | 2ndcredom 21631 | A second-countable space has at most the cardinality of the continuum. (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ (𝐽 ∈ 2nd𝜔 → 𝐽 ≼ ℝ) | ||
Theorem | 2ndc1stc 21632 | A second-countable space is first-countable. (Contributed by Jeff Hankins, 17-Jan-2010.) |
⊢ (𝐽 ∈ 2nd𝜔 → 𝐽 ∈ 1st𝜔) | ||
Theorem | 1stcrestlem 21633* | Lemma for 1stcrest 21634. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ (𝐵 ≼ ω → ran (𝑥 ∈ 𝐵 ↦ 𝐶) ≼ ω) | ||
Theorem | 1stcrest 21634 | A subspace of a first-countable space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ 1st𝜔) | ||
Theorem | 2ndcrest 21635 | A subspace of a second-countable space is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐽 ∈ 2nd𝜔 ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ 2nd𝜔) | ||
Theorem | 2ndcctbss 21636* | If a topology is second-countable, every base has a countable subset which is a base. Exercise 16B2 in Willard. (Contributed by Jeff Hankins, 28-Jan-2010.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
⊢ 𝐽 = (topGen‘𝐵) & ⊢ 𝑆 = {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣))} ⇒ ⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏))) | ||
Theorem | 2ndcdisj 21637* | Any disjoint family of open sets in a second-countable space is countable. (The sets are required to be nonempty because otherwise there could be many empty sets in the family.) (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.) |
⊢ ((𝐽 ∈ 2nd𝜔 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω) | ||
Theorem | 2ndcdisj2 21638* | Any disjoint collection of open sets in a second-countable space is countable. (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.) |
⊢ ((𝐽 ∈ 2nd𝜔 ∧ 𝐴 ⊆ 𝐽 ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝑥) → 𝐴 ≼ ω) | ||
Theorem | 2ndcomap 21639* | A surjective continuous open map maps second-countable spaces to second-countable spaces. (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐽 ∈ 2nd𝜔) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → ran 𝐹 = 𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ 𝐾) ⇒ ⊢ (𝜑 → 𝐾 ∈ 2nd𝜔) | ||
Theorem | 2ndcsep 21640* | A second-countable topology is separable, which is to say it contains a countable dense subset. (Contributed by Mario Carneiro, 13-Apr-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ 2nd𝜔 → ∃𝑥 ∈ 𝒫 𝑋(𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋)) | ||
Theorem | dis2ndc 21641 | A discrete space is second-countable iff it is countable. (Contributed by Mario Carneiro, 13-Apr-2015.) |
⊢ (𝑋 ≼ ω ↔ 𝒫 𝑋 ∈ 2nd𝜔) | ||
Theorem | 1stcelcls 21642* | A point belongs to the closure of a subset iff there is a sequence in the subset converging to it. Theorem 1.4-6(a) of [Kreyszig] p. 30. This proof uses countable choice ax-cc 9579. A space satisfying the conclusion of this theorem is called a sequential space, so the theorem can also be stated as "every first-countable space is a sequential space". (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃))) | ||
Theorem | 1stccnp 21643* | A mapping is continuous at 𝑃 in a first-countable space 𝑋 iff it is sequentially continuous at 𝑃, meaning that the image under 𝐹 of every sequence converging at 𝑃 converges to 𝐹(𝑃). This proof uses ax-cc 9579, but only via 1stcelcls 21642, so it could be refactored into a proof that continuity and sequential continuity are the same in sequential spaces. (Contributed by Mario Carneiro, 7-Sep-2015.) |
⊢ (𝜑 → 𝐽 ∈ 1st𝜔) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))))) | ||
Theorem | 1stccn 21644* | A mapping 𝑋⟶𝑌, where 𝑋 is first-countable, is continuous iff it is sequentially continuous, meaning that for any sequence 𝑓(𝑛) converging to 𝑥, its image under 𝐹 converges to 𝐹(𝑥). (Contributed by Mario Carneiro, 7-Sep-2015.) |
⊢ (𝜑 → 𝐽 ∈ 1st𝜔) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐹:𝑋⟶𝑌) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ∀𝑓(𝑓:ℕ⟶𝑋 → ∀𝑥(𝑓(⇝𝑡‘𝐽)𝑥 → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑥))))) | ||
Syntax | clly 21645 | Extend class notation with the "locally 𝐴 " predicate of a topological space. |
class Locally 𝐴 | ||
Syntax | cnlly 21646 | Extend class notation with the "N-locally 𝐴 " predicate of a topological space. |
class 𝑛-Locally 𝐴 | ||
Definition | df-lly 21647* | Define a space that is locally 𝐴, where 𝐴 is a topological property like "compact", "connected", or "path-connected". A topological space is locally 𝐴 if every neighborhood of a point contains an open sub-neighborhood that is 𝐴 in the subspace topology. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)} | ||
Definition | df-nlly 21648* |
Define a space that is n-locally 𝐴, where 𝐴 is a topological
property like "compact", "connected", or
"path-connected". A
topological space is n-locally 𝐴 if every neighborhood of a point
contains a sub-neighborhood that is 𝐴 in the subspace topology.
The terminology "n-locally", where 'n' stands for "neighborhood", is not standard, although this is sometimes called "weakly locally 𝐴". The reason for the distinction is that some notions only make sense for arbitrary neighborhoods (such as "locally compact", which is actually 𝑛-Locally Comp in our terminology - open compact sets are not very useful), while others such as "locally connected" are strictly weaker notions if the neighborhoods are not required to be open. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴} | ||
Theorem | islly 21649* | The property of being a locally 𝐴 topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐽 ∈ Locally 𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈ 𝐴))) | ||
Theorem | isnlly 21650* | The property of being an n-locally 𝐴 topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐽 ∈ 𝑛-Locally 𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)(𝐽 ↾t 𝑢) ∈ 𝐴)) | ||
Theorem | llyeq 21651 | Equality theorem for the Locally 𝐴 predicate. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐴 = 𝐵 → Locally 𝐴 = Locally 𝐵) | ||
Theorem | nllyeq 21652 | Equality theorem for the Locally 𝐴 predicate. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐴 = 𝐵 → 𝑛-Locally 𝐴 = 𝑛-Locally 𝐵) | ||
Theorem | llytop 21653 | A locally 𝐴 space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐽 ∈ Locally 𝐴 → 𝐽 ∈ Top) | ||
Theorem | nllytop 21654 | A locally 𝐴 space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐽 ∈ 𝑛-Locally 𝐴 → 𝐽 ∈ Top) | ||
Theorem | llyi 21655* | The property of a locally 𝐴 topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝐽 ∈ Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑢 ∈ 𝐽 (𝑢 ⊆ 𝑈 ∧ 𝑃 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈ 𝐴)) | ||
Theorem | nllyi 21656* | The property of an n-locally 𝐴 topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑃})(𝑢 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑢) ∈ 𝐴)) | ||
Theorem | nlly2i 21657* | Eliminate the neighborhood symbol from nllyi 21656. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑠 ∈ 𝒫 𝑈∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴)) | ||
Theorem | llynlly 21658 | A locally 𝐴 space is n-locally 𝐴: the "n-locally" predicate is the weaker notion. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐽 ∈ Locally 𝐴 → 𝐽 ∈ 𝑛-Locally 𝐴) | ||
Theorem | llyssnlly 21659 | A locally 𝐴 space is n-locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ Locally 𝐴 ⊆ 𝑛-Locally 𝐴 | ||
Theorem | llyss 21660 | The "locally" predicate respects inclusion. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐴 ⊆ 𝐵 → Locally 𝐴 ⊆ Locally 𝐵) | ||
Theorem | nllyss 21661 | The "n-locally" predicate respects inclusion. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐴 ⊆ 𝐵 → 𝑛-Locally 𝐴 ⊆ 𝑛-Locally 𝐵) | ||
Theorem | subislly 21662* | The property of a subspace being locally 𝐴. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ ((𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉) → ((𝐽 ↾t 𝐵) ∈ Locally 𝐴 ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ (𝑥 ∩ 𝐵)∃𝑢 ∈ 𝐽 ((𝑢 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝐽 ↾t (𝑢 ∩ 𝐵)) ∈ 𝐴))) | ||
Theorem | restnlly 21663* | If the property 𝐴 passes to open subspaces, then a space is n-locally 𝐴 iff it is locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗)) → (𝑗 ↾t 𝑥) ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑛-Locally 𝐴 = Locally 𝐴) | ||
Theorem | restlly 21664* | If the property 𝐴 passes to open subspaces, then a space which is 𝐴 is also locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗)) → (𝑗 ↾t 𝑥) ∈ 𝐴) & ⊢ (𝜑 → 𝐴 ⊆ Top) ⇒ ⊢ (𝜑 → 𝐴 ⊆ Locally 𝐴) | ||
Theorem | islly2 21665* | An alternative expression for 𝐽 ∈ Locally 𝐴 when 𝐴 passes to open subspaces: A space is locally 𝐴 if every point is contained in an open neighborhood with property 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗)) → (𝑗 ↾t 𝑥) ∈ 𝐴) & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝜑 → (𝐽 ∈ Locally 𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝑋 ∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈ 𝐴)))) | ||
Theorem | llyrest 21666 | An open subspace of a locally 𝐴 space is also locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽) → (𝐽 ↾t 𝐵) ∈ Locally 𝐴) | ||
Theorem | nllyrest 21667 | An open subspace of an n-locally 𝐴 space is also n-locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽) → (𝐽 ↾t 𝐵) ∈ 𝑛-Locally 𝐴) | ||
Theorem | loclly 21668 | If 𝐴 is a local property, then both Locally 𝐴 and 𝑛-Locally 𝐴 simplify to 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (Locally 𝐴 = 𝐴 ↔ 𝑛-Locally 𝐴 = 𝐴) | ||
Theorem | llyidm 21669 | Idempotence of the "locally" predicate, i.e. being "locally 𝐴 " is a local property. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ Locally Locally 𝐴 = Locally 𝐴 | ||
Theorem | nllyidm 21670 | Idempotence of the "n-locally" predicate, i.e. being "n-locally 𝐴 " is a local property. (Use loclly 21668 to show 𝑛-Locally 𝑛-Locally 𝐴 = 𝑛-Locally 𝐴.) (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ Locally 𝑛-Locally 𝐴 = 𝑛-Locally 𝐴 | ||
Theorem | toplly 21671 | A topology is locally a topology. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ Locally Top = Top | ||
Theorem | topnlly 21672 | A topology is n-locally a topology. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ 𝑛-Locally Top = Top | ||
Theorem | hauslly 21673 | A Hausdorff space is locally Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Locally Haus) | ||
Theorem | hausnlly 21674 | A Hausdorff space is n-locally Hausdorff iff it is locally Hausdorff (both notions are thus referred to as "locally Hausdorff"). (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐽 ∈ 𝑛-Locally Haus ↔ 𝐽 ∈ Locally Haus) | ||
Theorem | hausllycmp 21675 | A compact Hausdorff space is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) → 𝐽 ∈ 𝑛-Locally Comp) | ||
Theorem | cldllycmp 21676 | A closed subspace of a locally compact space is also locally compact. (The analogous result for open subspaces follows from the more general nllyrest 21667.) (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝐴) ∈ 𝑛-Locally Comp) | ||
Theorem | lly1stc 21677 | First-countability is a local property (unlike second-countability). (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ Locally 1st𝜔 = 1st𝜔 | ||
Theorem | dislly 21678* | The discrete space 𝒫 𝑋 is locally 𝐴 if and only if every singleton space has property 𝐴. (Contributed by Mario Carneiro, 20-Mar-2015.) |
⊢ (𝑋 ∈ 𝑉 → (𝒫 𝑋 ∈ Locally 𝐴 ↔ ∀𝑥 ∈ 𝑋 𝒫 {𝑥} ∈ 𝐴)) | ||
Theorem | disllycmp 21679 | A discrete space is locally compact. (Contributed by Mario Carneiro, 20-Mar-2015.) |
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Locally Comp) | ||
Theorem | dis1stc 21680 | A discrete space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ 1st𝜔) | ||
Theorem | hausmapdom 21681 | If 𝑋 is a first-countable Hausdorff space, then the cardinality of the closure of a set 𝐴 is bounded by ℕ to the power 𝐴. In particular, a first-countable Hausdorff space with a dense subset 𝐴 has cardinality at most 𝐴↑ℕ, and a separable first-countable Hausdorff space has cardinality at most 𝒫 ℕ. (Compare hauspwpwdom 22169 to see a weaker result if the assumption of first-countability is omitted.) (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔 ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘𝐴) ≼ (𝐴 ↑𝑚 ℕ)) | ||
Theorem | hauspwdom 21682 | Simplify the cardinal 𝐴↑ℕ of hausmapdom 21681 to 𝒫 𝐵 = 2↑𝐵 when 𝐵 is an infinite cardinal greater than 𝐴. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔 ∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → ((cls‘𝐽)‘𝐴) ≼ 𝒫 𝐵) | ||
Syntax | cref 21683 | Extend class definition to include the refinement relation. |
class Ref | ||
Syntax | cptfin 21684 | Extend class definition to include the class of point-finite covers. |
class PtFin | ||
Syntax | clocfin 21685 | Extend class definition to include the class of locally finite covers. |
class LocFin | ||
Definition | df-ref 21686* | Define the refinement relation. (Contributed by Jeff Hankins, 18-Jan-2010.) |
⊢ Ref = {〈𝑥, 𝑦〉 ∣ (∪ 𝑦 = ∪ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)} | ||
Definition | df-ptfin 21687* | Define "point-finite." (Contributed by Jeff Hankins, 21-Jan-2010.) |
⊢ PtFin = {𝑥 ∣ ∀𝑦 ∈ ∪ 𝑥{𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin} | ||
Definition | df-locfin 21688* | Define "locally finite." (Contributed by Jeff Hankins, 21-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
⊢ LocFin = (𝑥 ∈ Top ↦ {𝑦 ∣ (∪ 𝑥 = ∪ 𝑦 ∧ ∀𝑝 ∈ ∪ 𝑥∃𝑛 ∈ 𝑥 (𝑝 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))}) | ||
Theorem | refrel 21689 | Refinement is a relation. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
⊢ Rel Ref | ||
Theorem | isref 21690* | The property of being a refinement of a cover. Dr. Nyikos once commented in class that the term "refinement" is actually misleading and that people are inclined to confuse it with the notion defined in isfne 32867. On the other hand, the two concepts do seem to have a dual relationship. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
⊢ 𝑋 = ∪ 𝐴 & ⊢ 𝑌 = ∪ 𝐵 ⇒ ⊢ (𝐴 ∈ 𝐶 → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦))) | ||
Theorem | refbas 21691 | A refinement covers the same set. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
⊢ 𝑋 = ∪ 𝐴 & ⊢ 𝑌 = ∪ 𝐵 ⇒ ⊢ (𝐴Ref𝐵 → 𝑌 = 𝑋) | ||
Theorem | refssex 21692* | Every set in a refinement has a superset in the original cover. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
⊢ ((𝐴Ref𝐵 ∧ 𝑆 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 𝑆 ⊆ 𝑥) | ||
Theorem | ssref 21693 | A subcover is a refinement of the original cover. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
⊢ 𝑋 = ∪ 𝐴 & ⊢ 𝑌 = ∪ 𝐵 ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌) → 𝐴Ref𝐵) | ||
Theorem | refref 21694 | Reflexivity of refinement. (Contributed by Jeff Hankins, 18-Jan-2010.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴Ref𝐴) | ||
Theorem | reftr 21695 | Refinement is transitive. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → 𝐴Ref𝐶) | ||
Theorem | refun0 21696 | Adding the empty set preserves refinements. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
⊢ ((𝐴Ref𝐵 ∧ 𝐵 ≠ ∅) → (𝐴 ∪ {∅})Ref𝐵) | ||
Theorem | isptfin 21697* | The statement "is a point-finite cover." (Contributed by Jeff Hankins, 21-Jan-2010.) |
⊢ 𝑋 = ∪ 𝐴 ⇒ ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ PtFin ↔ ∀𝑥 ∈ 𝑋 {𝑦 ∈ 𝐴 ∣ 𝑥 ∈ 𝑦} ∈ Fin)) | ||
Theorem | islocfin 21698* | The statement "is a locally finite cover." (Contributed by Jeff Hankins, 21-Jan-2010.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐴 ⇒ ⊢ (𝐴 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))) | ||
Theorem | finptfin 21699 | A finite cover is a point-finite cover. (Contributed by Jeff Hankins, 21-Jan-2010.) |
⊢ (𝐴 ∈ Fin → 𝐴 ∈ PtFin) | ||
Theorem | ptfinfin 21700* | A point covered by a point-finite cover is only covered by finitely many elements. (Contributed by Jeff Hankins, 21-Jan-2010.) |
⊢ 𝑋 = ∪ 𝐴 ⇒ ⊢ ((𝐴 ∈ PtFin ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥} ∈ Fin) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |