Home | Metamath
Proof Explorer Theorem List (p. 209 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | resstps 20801 | 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 20802* | Lemma for ordtbas 20806. In a total order, unbounded-above intervals are closed under intersection. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 & ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) ⇒ ⊢ (𝑅 ∈ TosetRel → (fi‘𝐴) = 𝐴) | ||
Theorem | ordtval 20803* | Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 & ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) & ⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) ⇒ ⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) = (topGen‘(fi‘({𝑋} ∪ (𝐴 ∪ 𝐵))))) | ||
Theorem | ordtuni 20804* | Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 & ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) & ⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝑋 = ∪ ({𝑋} ∪ (𝐴 ∪ 𝐵))) | ||
Theorem | ordtbas2 20805* | Lemma for ordtbas 20806. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 & ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) & ⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) & ⊢ 𝐶 = ran (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)}) ⇒ ⊢ (𝑅 ∈ TosetRel → (fi‘(𝐴 ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∪ 𝐶)) | ||
Theorem | ordtbas 20806* | 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 20807 | Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) ∈ (TopOn‘𝑋)) | ||
Theorem | ordtopn1 20808* | An upward ray (𝑃, +∞) is open. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑃} ∈ (ordTop‘𝑅)) | ||
Theorem | ordtopn2 20809* | A downward ray (-∞, 𝑃) is open. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ¬ 𝑃𝑅𝑥} ∈ (ordTop‘𝑅)) | ||
Theorem | ordtopn3 20810* | An open interval (𝐴, 𝐵) is open. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ (¬ 𝑥𝑅𝐴 ∧ ¬ 𝐵𝑅𝑥)} ∈ (ordTop‘𝑅)) | ||
Theorem | ordtcld1 20811* | A downward ray (-∞, 𝑃] is closed. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ 𝑥𝑅𝑃} ∈ (Clsd‘(ordTop‘𝑅))) | ||
Theorem | ordtcld2 20812* | An upward ray [𝑃, +∞) is closed. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ 𝑃𝑅𝑥} ∈ (Clsd‘(ordTop‘𝑅))) | ||
Theorem | ordtcld3 20813* | A closed interval [𝐴, 𝐵] is closed. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ (𝐴𝑅𝑥 ∧ 𝑥𝑅𝐵)} ∈ (Clsd‘(ordTop‘𝑅))) | ||
Theorem | ordttop 20814 | The order topology is a topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) ∈ Top) | ||
Theorem | ordtcnv 20815 | The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝑅 ∈ PosetRel → (ordTop‘◡𝑅) = (ordTop‘𝑅)) | ||
Theorem | ordtrest 20816 | 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 20817* | Lemma for ordtrest2 20818. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 & ⊢ (𝜑 → 𝑅 ∈ TosetRel ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝑋 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} ⊆ 𝐴) ⇒ ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) | ||
Theorem | ordtrest2 20818* | 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 20819 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) | ||
Theorem | letop 20820 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (ordTop‘ ≤ ) ∈ Top | ||
Theorem | letopuni 20821 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ ℝ* = ∪ (ordTop‘ ≤ ) | ||
Theorem | xrstopn 20822 | The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (ordTop‘ ≤ ) = (TopOpen‘ℝ*𝑠) | ||
Theorem | xrstps 20823 | The extended real number structure is a topological space. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ℝ*𝑠 ∈ TopSp | ||
Theorem | leordtvallem1 20824* | Lemma for leordtval 20827. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ⇒ ⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ {𝑦 ∈ ℝ* ∣ ¬ 𝑦 ≤ 𝑥}) | ||
Theorem | leordtvallem2 20825* | Lemma for leordtval 20827. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) & ⊢ 𝐵 = ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥)) ⇒ ⊢ 𝐵 = ran (𝑥 ∈ ℝ* ↦ {𝑦 ∈ ℝ* ∣ ¬ 𝑥 ≤ 𝑦}) | ||
Theorem | leordtval2 20826 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) & ⊢ 𝐵 = ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥)) ⇒ ⊢ (ordTop‘ ≤ ) = (topGen‘(fi‘(𝐴 ∪ 𝐵))) | ||
Theorem | leordtval 20827 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) & ⊢ 𝐵 = ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥)) & ⊢ 𝐶 = ran (,) ⇒ ⊢ (ordTop‘ ≤ ) = (topGen‘((𝐴 ∪ 𝐵) ∪ 𝐶)) | ||
Theorem | iccordt 20828 | A closed interval is closed in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝐴[,]𝐵) ∈ (Clsd‘(ordTop‘ ≤ )) | ||
Theorem | iocpnfordt 20829 | 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 20830 | 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 20831 | An open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝐴(,)𝐵) ∈ (ordTop‘ ≤ ) | ||
Theorem | reordt 20832 | The real numbers are an open set in the topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ ℝ ∈ (ordTop‘ ≤ ) | ||
Theorem | lecldbas 20833 | 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 20834* | A neighborhood of +∞ contains an unbounded interval based at a real number. Together with xrtgioo 22417 (which describes neighborhoods of ℝ) and mnfnei 20835, this gives all "negative" topological information ensuring that it is not too fine (and of course iooordt 20831 and similar ensure that it has all the sets we want). (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ ((𝐴 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴) | ||
Theorem | mnfnei 20835* | A neighborhood of -∞ contains an unbounded interval based at a real number. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ ((𝐴 ∈ (ordTop‘ ≤ ) ∧ -∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴) | ||
Theorem | ordtrestixx 20836* | 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 20837 | 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 20838 | Extend class notation with the set of continuous functions between topologies. |
class Cn | ||
Syntax | ccnp 20839 | Extend class notation with the set of functions between topologies continuous at a point. |
class CnP | ||
Syntax | clm 20840 | 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 20841* | 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 20849 for the predicate form. (Contributed by NM, 17-Oct-2006.) |
⊢ Cn = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 (◡𝑓 “ 𝑦) ∈ 𝑗}) | ||
Definition | df-cnp 20842* | 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 ↦ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))})) | ||
Definition | df-lm 20843* | Define a function on topologies whose value is the convergence relation for the space. Although 𝑓 is typically a function from upper integers to the topological space, it doesn't have to be. Unfortunately, the value of the function must exist to use fvmpt 6191, and we use the otherwise unnecessary conjunct dom 𝑓 ⊆ ℂ to ensure that. (Contributed by NM, 7-Sep-2006.) |
⊢ ⇝𝑡 = (𝑗 ∈ Top ↦ {〈𝑓, 𝑥〉 ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))}) | ||
Theorem | lmrel 20844 | The topological space convergence relation is a relation. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
⊢ Rel (⇝𝑡‘𝐽) | ||
Theorem | lmrcl 20845 | Reverse closure for the convergence relation. (Contributed by Mario Carneiro, 7-Sep-2015.) |
⊢ (𝐹(⇝𝑡‘𝐽)𝑃 → 𝐽 ∈ Top) | ||
Theorem | lmfval 20846* | 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 20847* | 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 𝐾) = {𝑓 ∈ (𝑌 ↑𝑚 𝑋) ∣ ∀𝑦 ∈ 𝐾 (◡𝑓 “ 𝑦) ∈ 𝐽}) | ||
Theorem | cnpfval 20848* | 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 𝐾) = (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑𝑚 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))})) | ||
Theorem | iscn 20849* | The predicate "𝐹 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 20850* | 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 𝐾)‘𝑃) = {𝑓 ∈ (𝑌 ↑𝑚 𝑋) ∣ ∀𝑦 ∈ 𝐾 ((𝑓‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝑓 “ 𝑥) ⊆ 𝑦))}) | ||
Theorem | iscnp 20851* | The predicate "𝐹 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 20852* | The predicate "𝐹 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 20853* | The predicate "𝐹 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 20854 | Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) | ||
Theorem | cntop2 20855 | Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) | ||
Theorem | cnptop1 20856 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐽 ∈ Top) | ||
Theorem | cnptop2 20857 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐾 ∈ Top) | ||
Theorem | iscnp3 20858* | The predicate "𝐹 is a continuous function from topology 𝐽 to topology 𝐾 at point 𝑃." (Contributed by NM, 15-May-2007.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ (◡𝐹 “ 𝑦)))))) | ||
Theorem | cnprcl 20859 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝑃 ∈ 𝑋) | ||
Theorem | cnf 20860 | A continuous function is a mapping. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶𝑌) | ||
Theorem | cnpf 20861 | A continuous function at point 𝑃 is a mapping. (Contributed by FL, 17-Nov-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐹:𝑋⟶𝑌) | ||
Theorem | cnpcl 20862 | 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 20863 | A continuous function is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌) | ||
Theorem | cnpf2 20864 | A continuous function at point 𝑃 is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋⟶𝑌) | ||
Theorem | cnprcl2 20865 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑃 ∈ 𝑋) | ||
Theorem | tgcn 20866* | 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 20867* | 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 20868* | 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 20869 | 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 20870* | Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006.) |
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝐴) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝐴)) | ||
Theorem | idcn 20871 | 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 20872* | 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 20843. (Contributed by Mario Carneiro, 14-Nov-2013.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢)))) | ||
Theorem | lmbr2 20873* | 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 20874* | Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. This version of lmbr2 20873 presupposes that 𝐹 is a function. (Contributed by Mario Carneiro, 14-Nov-2013.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝐴 ∈ 𝑢)))) | ||
Theorem | lmconst 20875 | A constant sequence converges to its value. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ) → (𝑍 × {𝑃})(⇝𝑡‘𝐽)𝑃) | ||
Theorem | lmcvg 20876* | Convergence property of a converging sequence. (Contributed by Mario Carneiro, 14-Nov-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑃 ∈ 𝑈) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃) & ⊢ (𝜑 → 𝑈 ∈ 𝐽) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑈) | ||
Theorem | iscnp4 20877* | The predicate "𝐹 is a continuous function from topology 𝐽 to topology 𝐾 at point 𝑃." in terms of neighborhoods. (Contributed by FL, 18-Jul-2011.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦))) | ||
Theorem | cnpnei 20878* | A condition for continuity at a point in terms of neighborhoods. (Contributed by Jeff Hankins, 7-Sep-2009.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴}))) | ||
Theorem | cnima 20879 | An open subset of the codomain of a continuous function has an open preimage. (Contributed by FL, 15-Dec-2006.) |
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽) | ||
Theorem | cnco 20880 | The composition of two continuous functions is a continuous function. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐿)) → (𝐺 ∘ 𝐹) ∈ (𝐽 Cn 𝐿)) | ||
Theorem | cnpco 20881 | The composition of two continuous functions at point 𝑃 is a continuous function at point 𝑃. Proposition of [BourbakiTop1] p. I.9. (Contributed by FL, 16-Nov-2006.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃))) → (𝐺 ∘ 𝐹) ∈ ((𝐽 CnP 𝐿)‘𝑃)) | ||
Theorem | cnclima 20882 | A closed subset of the codomain of a continuous function has a closed preimage. (Contributed by NM, 15-Mar-2007.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsd‘𝐾)) → (◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽)) | ||
Theorem | iscncl 20883* | A definition of a continuous function using closed sets. Theorem 1 (d) of [BourbakiTop1] p. I.9. (Contributed by FL, 19-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(◡𝐹 “ 𝑦) ∈ (Clsd‘𝐽)))) | ||
Theorem | cncls2i 20884 | Property of the preimage of a closure. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑌) → ((cls‘𝐽)‘(◡𝐹 “ 𝑆)) ⊆ (◡𝐹 “ ((cls‘𝐾)‘𝑆))) | ||
Theorem | cnntri 20885 | Property of the preimage of an interior. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑌) → (◡𝐹 “ ((int‘𝐾)‘𝑆)) ⊆ ((int‘𝐽)‘(◡𝐹 “ 𝑆))) | ||
Theorem | cnclsi 20886 | Property of the image of a closure. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑋) → (𝐹 “ ((cls‘𝐽)‘𝑆)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑆))) | ||
Theorem | cncls2 20887* | Continuity in terms of closure. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝒫 𝑌((cls‘𝐽)‘(◡𝐹 “ 𝑥)) ⊆ (◡𝐹 “ ((cls‘𝐾)‘𝑥))))) | ||
Theorem | cncls 20888* | Continuity in terms of closure. (Contributed by Jeff Hankins, 1-Oct-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝒫 𝑋(𝐹 “ ((cls‘𝐽)‘𝑥)) ⊆ ((cls‘𝐾)‘(𝐹 “ 𝑥))))) | ||
Theorem | cnntr 20889* | Continuity in terms of interior. (Contributed by Jeff Hankins, 2-Oct-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝒫 𝑌(◡𝐹 “ ((int‘𝐾)‘𝑥)) ⊆ ((int‘𝐽)‘(◡𝐹 “ 𝑥))))) | ||
Theorem | cnss1 20890 | If the topology 𝐾 is finer than 𝐽, then there are more continuous functions from 𝐾 than from 𝐽. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (𝐽 Cn 𝐿) ⊆ (𝐾 Cn 𝐿)) | ||
Theorem | cnss2 20891 | If the topology 𝐾 is finer than 𝐽, then there are fewer continuous functions into 𝐾 than into 𝐽 from some other space. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ ((𝐿 ∈ (TopOn‘𝑌) ∧ 𝐿 ⊆ 𝐾) → (𝐽 Cn 𝐾) ⊆ (𝐽 Cn 𝐿)) | ||
Theorem | cncnpi 20892 | A continuous function is continuous at all points. One direction of Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ 𝑋) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) | ||
Theorem | cnsscnp 20893 | The set of continuous functions is a subset of the set of continuous functions at a point. (Contributed by Raph Levien, 21-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝑃 ∈ 𝑋 → (𝐽 Cn 𝐾) ⊆ ((𝐽 CnP 𝐾)‘𝑃)) | ||
Theorem | cncnp 20894* | A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 15-May-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥)))) | ||
Theorem | cncnp2 20895* | A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (𝑋 ≠ ∅ → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) | ||
Theorem | cnnei 20896* | Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux, 3-Jan-2018.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ∀𝑝 ∈ 𝑋 ∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑝)})∃𝑣 ∈ ((nei‘𝐽)‘{𝑝})(𝐹 “ 𝑣) ⊆ 𝑤)) | ||
Theorem | cnconst2 20897 | A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐵 ∈ 𝑌) → (𝑋 × {𝐵}) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | cnconst 20898 | A constant function is continuous. (Contributed by FL, 15-Jan-2007.) (Proof shortened by Mario Carneiro, 19-Mar-2015.) |
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐵 ∈ 𝑌 ∧ 𝐹:𝑋⟶{𝐵})) → 𝐹 ∈ (𝐽 Cn 𝐾)) | ||
Theorem | cnrest 20899 | Continuity of a restriction from a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) | ||
Theorem | cnrest2 20900 | Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Hankins, 10-Jul-2009.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |