Home | Metamath
Proof Explorer Theorem List (p. 218 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 | stoig 21701 | The topological space built with a subspace topology. (Contributed by FL, 5-Jan-2009.) (Proof shortened by Mario Carneiro, 1-May-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), (𝐽 ↾t 𝐴)〉} ∈ TopSp) | ||
Theorem | restco 21702 | Composition of subspaces. (Contributed by Mario Carneiro, 15-Dec-2013.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ((𝐽 ↾t 𝐴) ↾t 𝐵) = (𝐽 ↾t (𝐴 ∩ 𝐵))) | ||
Theorem | restabs 21703 | Equivalence of being a subspace of a subspace and being a subspace of the original. (Contributed by Jeff Hankins, 11-Jul-2009.) (Proof shortened by Mario Carneiro, 1-May-2015.) |
⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑊) → ((𝐽 ↾t 𝑇) ↾t 𝑆) = (𝐽 ↾t 𝑆)) | ||
Theorem | restin 21704 | When the subspace region is not a subset of the base of the topology, the resulting set is the same as the subspace restricted to the base. (Contributed by Mario Carneiro, 15-Dec-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝐽 ↾t 𝐴) = (𝐽 ↾t (𝐴 ∩ 𝑋))) | ||
Theorem | restuni2 21705 | The underlying set of a subspace topology. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝑋) = ∪ (𝐽 ↾t 𝐴)) | ||
Theorem | resttopon2 21706 | The underlying set of a subspace topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ (TopOn‘(𝐴 ∩ 𝑋))) | ||
Theorem | rest0 21707 | The subspace topology induced by the topology 𝐽 on the empty set. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ (𝐽 ∈ Top → (𝐽 ↾t ∅) = {∅}) | ||
Theorem | restsn 21708 | The only subspace topology induced by the topology {∅}. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ (𝐴 ∈ 𝑉 → ({∅} ↾t 𝐴) = {∅}) | ||
Theorem | restsn2 21709 | The subspace topology induced by a singleton. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 16-Sep-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t {𝐴}) = 𝒫 {𝐴}) | ||
Theorem | restcld 21710* | A closed set of a subspace topology is a closed set of the original topology intersected with the subset. (Contributed by FL, 11-Jul-2009.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∈ (Clsd‘(𝐽 ↾t 𝑆)) ↔ ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆))) | ||
Theorem | restcldi 21711 | A closed set is closed in the subspace topology. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ (Clsd‘𝐽) ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ (Clsd‘(𝐽 ↾t 𝐴))) | ||
Theorem | restcldr 21712 | A set which is closed in the subspace topology induced by a closed set is closed in the original topology. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐴 ∈ (Clsd‘𝐽) ∧ 𝐵 ∈ (Clsd‘(𝐽 ↾t 𝐴))) → 𝐵 ∈ (Clsd‘𝐽)) | ||
Theorem | restopnb 21713 | If 𝐵 is an open subset of the subspace base set 𝐴, then any subset of 𝐵 is open iff it is open in 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝐽 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐵)) → (𝐶 ∈ 𝐽 ↔ 𝐶 ∈ (𝐽 ↾t 𝐴))) | ||
Theorem | ssrest 21714 | If 𝐾 is a finer topology than 𝐽, then the subspace topologies induced by 𝐴 maintain this relationship. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ ((𝐾 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐾) → (𝐽 ↾t 𝐴) ⊆ (𝐾 ↾t 𝐴)) | ||
Theorem | restopn2 21715 | If 𝐴 is open, then 𝐵 is open in 𝐴 iff it is an open subset of 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → (𝐵 ∈ (𝐽 ↾t 𝐴) ↔ (𝐵 ∈ 𝐽 ∧ 𝐵 ⊆ 𝐴))) | ||
Theorem | restdis 21716 | A subspace of a discrete topology is discrete. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → (𝒫 𝐴 ↾t 𝐵) = 𝒫 𝐵) | ||
Theorem | restfpw 21717 | The restriction of the set of finite subsets of 𝐴 is the set of finite subsets of 𝐵. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → ((𝒫 𝐴 ∩ Fin) ↾t 𝐵) = (𝒫 𝐵 ∩ Fin)) | ||
Theorem | neitr 21718 | The neighborhood of a trace is the trace of the neighborhood. (Contributed by Thierry Arnoux, 17-Jan-2018.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((nei‘(𝐽 ↾t 𝐴))‘𝐵) = (((nei‘𝐽)‘𝐵) ↾t 𝐴)) | ||
Theorem | restcls 21719 | A closure in a subspace topology. (Contributed by Jeff Hankins, 22-Jan-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (𝐽 ↾t 𝑌) ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((cls‘𝐾)‘𝑆) = (((cls‘𝐽)‘𝑆) ∩ 𝑌)) | ||
Theorem | restntr 21720 | An interior in a subspace topology. Willard in General Topology says that there is no analogue of restcls 21719 for interiors. In some sense, that is true. (Contributed by Jeff Hankins, 23-Jan-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (𝐽 ↾t 𝑌) ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((int‘𝐾)‘𝑆) = (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌)) | ||
Theorem | restlp 21721 | The limit points of a subset restrict naturally in a subspace. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (𝐽 ↾t 𝑌) ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((limPt‘𝐾)‘𝑆) = (((limPt‘𝐽)‘𝑆) ∩ 𝑌)) | ||
Theorem | restperf 21722 | Perfection of a subspace. Note that the term "perfect set" is reserved for closed sets which are perfect in the subspace topology. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (𝐽 ↾t 𝑌) ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋) → (𝐾 ∈ Perf ↔ 𝑌 ⊆ ((limPt‘𝐽)‘𝑌))) | ||
Theorem | perfopn 21723 | An open subset of a perfect space is perfect. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (𝐽 ↾t 𝑌) ⇒ ⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → 𝐾 ∈ Perf) | ||
Theorem | resstopn 21724 | The topology of a restricted structure. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐻 = (𝐾 ↾s 𝐴) & ⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐽 ↾t 𝐴) = (TopOpen‘𝐻) | ||
Theorem | resstps 21725 | A restricted topological space is a topological space. Note that this theorem would not be true if TopSp was defined directly in terms of the TopSet slot instead of the TopOpen derived function. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ ((𝐾 ∈ TopSp ∧ 𝐴 ∈ 𝑉) → (𝐾 ↾s 𝐴) ∈ TopSp) | ||
Theorem | ordtbaslem 21726* | Lemma for ordtbas 21730. In a total order, unbounded-above intervals are closed under intersection. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 & ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) ⇒ ⊢ (𝑅 ∈ TosetRel → (fi‘𝐴) = 𝐴) | ||
Theorem | ordtval 21727* | Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 & ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) & ⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) ⇒ ⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) = (topGen‘(fi‘({𝑋} ∪ (𝐴 ∪ 𝐵))))) | ||
Theorem | ordtuni 21728* | Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 & ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) & ⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝑋 = ∪ ({𝑋} ∪ (𝐴 ∪ 𝐵))) | ||
Theorem | ordtbas2 21729* | Lemma for ordtbas 21730. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 & ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) & ⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) & ⊢ 𝐶 = ran (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)}) ⇒ ⊢ (𝑅 ∈ TosetRel → (fi‘(𝐴 ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∪ 𝐶)) | ||
Theorem | ordtbas 21730* | In a total order, the finite intersections of the open rays generates the set of open intervals, but no more - these four collections form a subbasis for the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 & ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) & ⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) & ⊢ 𝐶 = ran (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)}) ⇒ ⊢ (𝑅 ∈ TosetRel → (fi‘({𝑋} ∪ (𝐴 ∪ 𝐵))) = (({𝑋} ∪ (𝐴 ∪ 𝐵)) ∪ 𝐶)) | ||
Theorem | ordttopon 21731 | Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) ∈ (TopOn‘𝑋)) | ||
Theorem | ordtopn1 21732* | An upward ray (𝑃, +∞) is open. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑃} ∈ (ordTop‘𝑅)) | ||
Theorem | ordtopn2 21733* | A downward ray (-∞, 𝑃) is open. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ¬ 𝑃𝑅𝑥} ∈ (ordTop‘𝑅)) | ||
Theorem | ordtopn3 21734* | An open interval (𝐴, 𝐵) is open. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ (¬ 𝑥𝑅𝐴 ∧ ¬ 𝐵𝑅𝑥)} ∈ (ordTop‘𝑅)) | ||
Theorem | ordtcld1 21735* | A downward ray (-∞, 𝑃] is closed. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ 𝑥𝑅𝑃} ∈ (Clsd‘(ordTop‘𝑅))) | ||
Theorem | ordtcld2 21736* | An upward ray [𝑃, +∞) is closed. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ 𝑃𝑅𝑥} ∈ (Clsd‘(ordTop‘𝑅))) | ||
Theorem | ordtcld3 21737* | A closed interval [𝐴, 𝐵] is closed. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ (𝐴𝑅𝑥 ∧ 𝑥𝑅𝐵)} ∈ (Clsd‘(ordTop‘𝑅))) | ||
Theorem | ordttop 21738 | The order topology is a topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) ∈ Top) | ||
Theorem | ordtcnv 21739 | The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝑅 ∈ PosetRel → (ordTop‘◡𝑅) = (ordTop‘𝑅)) | ||
Theorem | ordtrest 21740 | The subspace topology of an order topology is in general finer than the topology generated by the restricted order, but we do have inclusion in one direction. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ⊆ ((ordTop‘𝑅) ↾t 𝐴)) | ||
Theorem | ordtrest2lem 21741* | Lemma for ordtrest2 21742. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 & ⊢ (𝜑 → 𝑅 ∈ TosetRel ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝑋 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} ⊆ 𝐴) ⇒ ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | ||
Theorem | ordtrest2 21742* | An interval-closed set 𝐴 in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in ℝ, but in other sets like ℚ there are interval-closed sets like (π, +∞) ∩ ℚ that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 & ⊢ (𝜑 → 𝑅 ∈ TosetRel ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝑋 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} ⊆ 𝐴) ⇒ ⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) = ((ordTop‘𝑅) ↾t 𝐴)) | ||
Theorem | letopon 21743 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) | ||
Theorem | letop 21744 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (ordTop‘ ≤ ) ∈ Top | ||
Theorem | letopuni 21745 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ ℝ* = ∪ (ordTop‘ ≤ ) | ||
Theorem | xrstopn 21746 | The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (ordTop‘ ≤ ) = (TopOpen‘ℝ*𝑠) | ||
Theorem | xrstps 21747 | The extended real number structure is a topological space. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ℝ*𝑠 ∈ TopSp | ||
Theorem | leordtvallem1 21748* | Lemma for leordtval 21751. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ⇒ ⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ {𝑦 ∈ ℝ* ∣ ¬ 𝑦 ≤ 𝑥}) | ||
Theorem | leordtvallem2 21749* | Lemma for leordtval 21751. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) & ⊢ 𝐵 = ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥)) ⇒ ⊢ 𝐵 = ran (𝑥 ∈ ℝ* ↦ {𝑦 ∈ ℝ* ∣ ¬ 𝑥 ≤ 𝑦}) | ||
Theorem | leordtval2 21750 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) & ⊢ 𝐵 = ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥)) ⇒ ⊢ (ordTop‘ ≤ ) = (topGen‘(fi‘(𝐴 ∪ 𝐵))) | ||
Theorem | leordtval 21751 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) & ⊢ 𝐵 = ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥)) & ⊢ 𝐶 = ran (,) ⇒ ⊢ (ordTop‘ ≤ ) = (topGen‘((𝐴 ∪ 𝐵) ∪ 𝐶)) | ||
Theorem | iccordt 21752 | A closed interval is closed in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝐴[,]𝐵) ∈ (Clsd‘(ordTop‘ ≤ )) | ||
Theorem | iocpnfordt 21753 | An unbounded above open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝐴(,]+∞) ∈ (ordTop‘ ≤ ) | ||
Theorem | icomnfordt 21754 | An unbounded above open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (-∞[,)𝐴) ∈ (ordTop‘ ≤ ) | ||
Theorem | iooordt 21755 | An open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝐴(,)𝐵) ∈ (ordTop‘ ≤ ) | ||
Theorem | reordt 21756 | The real numbers are an open set in the topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ ℝ ∈ (ordTop‘ ≤ ) | ||
Theorem | lecldbas 21757 | The set of closed intervals forms a closed subbasis for the topology on the extended reals. Since our definition of a basis is in terms of open sets, we express this by showing that the complements of closed intervals form an open subbasis for the topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ ran [,] ↦ (ℝ* ∖ 𝑥)) ⇒ ⊢ (ordTop‘ ≤ ) = (topGen‘(fi‘ran 𝐹)) | ||
Theorem | pnfnei 21758* | A neighborhood of +∞ contains an unbounded interval based at a real number. Together with xrtgioo 23343 (which describes neighborhoods of ℝ) and mnfnei 21759, this gives all "negative" topological information ensuring that it is not too fine (and of course iooordt 21755 and similar ensure that it has all the sets we want). (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ ((𝐴 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴) | ||
Theorem | mnfnei 21759* | A neighborhood of -∞ contains an unbounded interval based at a real number. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ ((𝐴 ∈ (ordTop‘ ≤ ) ∧ -∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴) | ||
Theorem | ordtrestixx 21760* | The restriction of the less than order to an interval gives the same topology as the subspace topology. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝐴 ⊆ ℝ* & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥[,]𝑦) ⊆ 𝐴) ⇒ ⊢ ((ordTop‘ ≤ ) ↾t 𝐴) = (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) | ||
Theorem | ordtresticc 21761 | The restriction of the less than order to a closed interval gives the same topology as the subspace topology. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ ((ordTop‘ ≤ ) ↾t (𝐴[,]𝐵)) = (ordTop‘( ≤ ∩ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) | ||
Syntax | ccn 21762 | Extend class notation with the class of continuous functions between topologies. |
class Cn | ||
Syntax | ccnp 21763 | Extend class notation with the class of functions between topologies continuous at a given point. |
class CnP | ||
Syntax | clm 21764 | Extend class notation with a function on topological spaces whose value is the convergence relation for limit sequences in the space. |
class ⇝𝑡 | ||
Definition | df-cn 21765* | Define a function on two topologies whose value is the set of continuous mappings from the first topology to the second. Based on definition of continuous function in [Munkres] p. 102. See iscn 21773 for the predicate form. (Contributed by NM, 17-Oct-2006.) |
⊢ Cn = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 (◡𝑓 “ 𝑦) ∈ 𝑗}) | ||
Definition | df-cnp 21766* | Define a function on two topologies whose value is the set of continuous mappings at a specified point in the first topology. Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 17-Oct-2006.) |
⊢ CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))})) | ||
Definition | df-lm 21767* | Define a function on topologies whose value is the convergence relation for sequences into the given topological space. Although 𝑓 is typically a sequence (a function from an upperset of integers) with values in the topological space, it need not be. Note, however, that the limit property concerns only values at integers, so that the real-valued function (𝑥 ∈ ℝ ↦ (sin‘(π · 𝑥))) converges to zero (in the standard topology on the reals) with this definition. (Contributed by NM, 7-Sep-2006.) |
⊢ ⇝𝑡 = (𝑗 ∈ Top ↦ {〈𝑓, 𝑥〉 ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))}) | ||
Theorem | lmrel 21768 | The topological space convergence relation is a relation. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
⊢ Rel (⇝𝑡‘𝐽) | ||
Theorem | lmrcl 21769 | Reverse closure for the convergence relation. (Contributed by Mario Carneiro, 7-Sep-2015.) |
⊢ (𝐹(⇝𝑡‘𝐽)𝑃 → 𝐽 ∈ Top) | ||
Theorem | lmfval 21770* | The relation "sequence 𝑓 converges to point 𝑦 " in a metric space. (Contributed by NM, 7-Sep-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → (⇝𝑡‘𝐽) = {〈𝑓, 𝑥〉 ∣ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧ 𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))}) | ||
Theorem | cnfval 21771* | The set of all continuous functions from topology 𝐽 to topology 𝐾. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 Cn 𝐾) = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑦 ∈ 𝐾 (◡𝑓 “ 𝑦) ∈ 𝐽}) | ||
Theorem | cnpfval 21772* | The function mapping the points in a topology 𝐽 to the set of all functions from 𝐽 to topology 𝐾 continuous at that point. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 CnP 𝐾) = (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))})) | ||
Theorem | iscn 21773* | The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾". Definition of continuous function in [Munkres] p. 102. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽))) | ||
Theorem | cnpval 21774* | The set of all functions from topology 𝐽 to topology 𝐾 that are continuous at a point 𝑃. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → ((𝐽 CnP 𝐾)‘𝑃) = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑦 ∈ 𝐾 ((𝑓‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝑓 “ 𝑥) ⊆ 𝑦))}) | ||
Theorem | iscnp 21775* | The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾 at point 𝑃". Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦))))) | ||
Theorem | iscn2 21776* | The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾". Definition of continuous function in [Munkres] p. 102. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽))) | ||
Theorem | iscnp2 21777* | The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾 at point 𝑃". Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦))))) | ||
Theorem | cntop1 21778 | Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) | ||
Theorem | cntop2 21779 | Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) | ||
Theorem | cnptop1 21780 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐽 ∈ Top) | ||
Theorem | cnptop2 21781 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐾 ∈ Top) | ||
Theorem | iscnp3 21782* | The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾 at point 𝑃". (Contributed by NM, 15-May-2007.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ (◡𝐹 “ 𝑦)))))) | ||
Theorem | cnprcl 21783 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝑃 ∈ 𝑋) | ||
Theorem | cnf 21784 | A continuous function is a mapping. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶𝑌) | ||
Theorem | cnpf 21785 | A continuous function at point 𝑃 is a mapping. (Contributed by FL, 17-Nov-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐹:𝑋⟶𝑌) | ||
Theorem | cnpcl 21786 | The value of a continuous function from 𝐽 to 𝐾 at point 𝑃 belongs to the underlying set of topology 𝐾. (Contributed by FL, 27-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ∈ 𝑌) | ||
Theorem | cnf2 21787 | A continuous function is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌) | ||
Theorem | cnpf2 21788 | A continuous function at point 𝑃 is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋⟶𝑌) | ||
Theorem | cnprcl2 21789 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑃 ∈ 𝑋) | ||
Theorem | tgcn 21790* | The continuity predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 = (topGen‘𝐵)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽))) | ||
Theorem | tgcnp 21791* | The "continuous at a point" predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 = (topGen‘𝐵)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐵 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦))))) | ||
Theorem | subbascn 21792* | The continuity predicate when the range is given by a subbasis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐾 = (topGen‘(fi‘𝐵))) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽))) | ||
Theorem | ssidcn 21793 | The identity function is a continuous function from one topology to another topology on the same set iff the domain is finer than the codomain. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) → (( I ↾ 𝑋) ∈ (𝐽 Cn 𝐾) ↔ 𝐾 ⊆ 𝐽)) | ||
Theorem | cnpimaex 21794* | Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006.) |
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝐴) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝐴)) | ||
Theorem | idcn 21795 | A restricted identity function is a continuous function. (Contributed by FL, 27-Dec-2006.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → ( I ↾ 𝑋) ∈ (𝐽 Cn 𝐽)) | ||
Theorem | lmbr 21796* | Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a topological space. Definition 1.4-1 of [Kreyszig] p. 25. The condition 𝐹 ⊆ (ℂ × 𝑋) allows us to use objects more general than sequences when convenient; see the comment in df-lm 21767. (Contributed by Mario Carneiro, 14-Nov-2013.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢)))) | ||
Theorem | lmbr2 21797* | Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. (Contributed by Mario Carneiro, 14-Nov-2013.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))))) | ||
Theorem | lmbrf 21798* | Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. This version of lmbr2 21797 presupposes that 𝐹 is a function. (Contributed by Mario Carneiro, 14-Nov-2013.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝐴 ∈ 𝑢)))) | ||
Theorem | lmconst 21799 | A constant sequence converges to its value. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ) → (𝑍 × {𝑃})(⇝𝑡‘𝐽)𝑃) | ||
Theorem | lmcvg 21800* | Convergence property of a converging sequence. (Contributed by Mario Carneiro, 14-Nov-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑃 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃) & ⊢ (𝜑 → 𝑈 ∈ 𝐽) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑈) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |