Theorem List for Intuitionistic Logic Explorer - 13501-13600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | clsss3 13501 |
The closure of a subset of a topological space is included in the space.
(Contributed by NM, 26-Feb-2007.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋) |
|
Theorem | ntrcls0 13502 |
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 13503* |
Two ways to say that a subset has an empty interior. (Contributed by
NM, 3-Oct-2007.) (Revised by Jim Kingdon, 11-Mar-2023.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (((int‘𝐽)‘𝑆) = ∅ ↔ ∀𝑥 ∈ 𝐽 (𝑥 ⊆ 𝑆 → 𝑥 = ∅))) |
|
Theorem | cls0 13504 |
The closure of the empty set. (Contributed by NM, 2-Oct-2007.) (Proof
shortened by Jim Kingdon, 12-Mar-2023.)
|
⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘∅) =
∅) |
|
Theorem | ntr0 13505 |
The interior of the empty set. (Contributed by NM, 2-Oct-2007.)
|
⊢ (𝐽 ∈ Top → ((int‘𝐽)‘∅) =
∅) |
|
Theorem | isopn3i 13506 |
An open subset equals its own interior. (Contributed by Mario Carneiro,
30-Dec-2016.)
|
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → ((int‘𝐽)‘𝑆) = 𝑆) |
|
Theorem | discld 13507 |
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 13508 |
The closed sets of the topology {∅}.
(Contributed by FL,
5-Jan-2009.)
|
⊢ (Clsd‘{∅}) =
{∅} |
|
8.1.5 Neighborhoods
|
|
Syntax | cnei 13509 |
Extend class notation with neighborhood relation for topologies.
|
class nei |
|
Definition | df-nei 13510* |
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 13511* |
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 13512 |
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 13513 |
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 13514* |
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 13515* |
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 13516 |
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 13517* |
The predicate "the class 𝑁 is a neighborhood of point 𝑃".
(Contributed by NM, 26-Feb-2007.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ 𝑋 ∧ ∃𝑔 ∈ 𝐽 (𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁)))) |
|
Theorem | neii1 13518 |
A neighborhood is included in the topology's base set. (Contributed by
NM, 12-Feb-2007.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑁 ⊆ 𝑋) |
|
Theorem | neisspw 13519 |
The neighborhoods of any set are subsets of the base set. (Contributed
by Stefan O'Rear, 6-Aug-2015.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘𝑆) ⊆ 𝒫 𝑋) |
|
Theorem | neii2 13520* |
Property of a neighborhood. (Contributed by NM, 12-Feb-2007.)
|
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → ∃𝑔 ∈ 𝐽 (𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁)) |
|
Theorem | neiss 13521 |
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 13522 |
A set is included in any of its neighborhoods. Generalization to
subsets of elnei 13523. (Contributed by FL, 16-Nov-2006.)
|
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑁) |
|
Theorem | elnei 13523 |
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 13524 |
The empty set is not a neighborhood of a nonempty set. (Contributed by
FL, 18-Sep-2007.)
|
⊢ ((𝐽 ∈ Top ∧ 𝑆 ≠ ∅) → ¬ ∅ ∈
((nei‘𝐽)‘𝑆)) |
|
Theorem | neipsm 13525* |
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.) (Revised by Jim Kingdon, 22-Mar-2023.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ ∃𝑥 𝑥 ∈ 𝑆) → (𝑁 ∈ ((nei‘𝐽)‘𝑆) ↔ ∀𝑝 ∈ 𝑆 𝑁 ∈ ((nei‘𝐽)‘{𝑝}))) |
|
Theorem | opnneissb 13526 |
An open set is a neighborhood of any of its subsets. (Contributed by
FL, 2-Oct-2006.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋) → (𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ((nei‘𝐽)‘𝑆))) |
|
Theorem | opnssneib 13527 |
Any superset of an open set is a neighborhood of it. (Contributed by
NM, 14-Feb-2007.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ∧ 𝑁 ⊆ 𝑋) → (𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ((nei‘𝐽)‘𝑆))) |
|
Theorem | ssnei2 13528 |
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 | opnneiss 13529 |
An open set is a neighborhood of any of its subsets. (Contributed by NM,
13-Feb-2007.)
|
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘𝑆)) |
|
Theorem | opnneip 13530 |
An open set is a neighborhood of any of its members. (Contributed by NM,
8-Mar-2007.)
|
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑃 ∈ 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) |
|
Theorem | tpnei 13531 |
The underlying set of a topology is a neighborhood of any of its
subsets. Special case of opnneiss 13529. (Contributed by FL,
2-Oct-2006.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (𝑆 ⊆ 𝑋 ↔ 𝑋 ∈ ((nei‘𝐽)‘𝑆))) |
|
Theorem | neiuni 13532 |
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 | topssnei 13533 |
A finer topology has more neighborhoods. (Contributed by Mario
Carneiro, 9-Apr-2015.)
|
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪
𝐾
⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌) ∧ 𝐽 ⊆ 𝐾) → ((nei‘𝐽)‘𝑆) ⊆ ((nei‘𝐾)‘𝑆)) |
|
Theorem | innei 13534 |
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 13535 |
Only an open set is a neighborhood of itself. (Contributed by FL,
2-Oct-2006.)
|
⊢ (𝐽 ∈ Top → (𝑁 ∈ ((nei‘𝐽)‘𝑁) ↔ 𝑁 ∈ 𝐽)) |
|
Theorem | neissex 13536* |
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 13537 |
The empty set is a neighborhood of itself. (Contributed by FL,
10-Dec-2006.)
|
⊢ (𝐽 ∈ Top → ∅ ∈
((nei‘𝐽)‘∅)) |
|
8.1.6 Subspace topologies
|
|
Theorem | restrcl 13538 |
Reverse closure for the subspace topology. (Contributed by Mario
Carneiro, 19-Mar-2015.) (Proof shortened by Jim Kingdon,
23-Mar-2023.)
|
⊢ ((𝐽 ↾t 𝐴) ∈ Top → (𝐽 ∈ V ∧ 𝐴 ∈ V)) |
|
Theorem | restbasg 13539 |
A subspace topology basis is a basis. (Contributed by Mario Carneiro,
19-Mar-2015.)
|
⊢ ((𝐵 ∈ TopBases ∧ 𝐴 ∈ 𝑉) → (𝐵 ↾t 𝐴) ∈ TopBases) |
|
Theorem | tgrest 13540 |
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 13541 |
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 13542 |
A subspace topology is a topology on the base set. (Contributed by
Mario Carneiro, 13-Aug-2015.)
|
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴)) |
|
Theorem | restuni 13543 |
The underlying set of a subspace topology. (Contributed by FL,
5-Jan-2009.) (Revised by Mario Carneiro, 13-Aug-2015.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
|
Theorem | stoig 13544 |
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 13545 |
Composition of subspaces. (Contributed by Mario Carneiro, 15-Dec-2013.)
(Revised by Mario Carneiro, 1-May-2015.)
|
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ((𝐽 ↾t 𝐴) ↾t 𝐵) = (𝐽 ↾t (𝐴 ∩ 𝐵))) |
|
Theorem | restabs 13546 |
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 13547 |
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 13548 |
The underlying set of a subspace topology. (Contributed by Mario
Carneiro, 21-Mar-2015.)
|
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝑋) = ∪ (𝐽 ↾t 𝐴)) |
|
Theorem | resttopon2 13549 |
The underlying set of a subspace topology. (Contributed by Mario
Carneiro, 13-Aug-2015.)
|
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ (TopOn‘(𝐴 ∩ 𝑋))) |
|
Theorem | rest0 13550 |
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 13551 |
The only subspace topology induced by the topology {∅}.
(Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro,
15-Dec-2013.)
|
⊢ (𝐴 ∈ 𝑉 → ({∅} ↾t
𝐴) =
{∅}) |
|
Theorem | restopnb 13552 |
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 13553 |
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 13554 |
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 13555 |
A subspace of a discrete topology is discrete. (Contributed by Mario
Carneiro, 19-Mar-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → (𝒫 𝐴 ↾t 𝐵) = 𝒫 𝐵) |
|
8.1.7 Limits and continuity in topological
spaces
|
|
Syntax | ccn 13556 |
Extend class notation with the class of continuous functions between
topologies.
|
class Cn |
|
Syntax | ccnp 13557 |
Extend class notation with the class of functions between topologies
continuous at a given point.
|
class CnP |
|
Syntax | clm 13558 |
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 13559* |
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 13568 for the predicate
form. (Contributed by NM, 17-Oct-2006.)
|
⊢ Cn = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚
∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 (◡𝑓 “ 𝑦) ∈ 𝑗}) |
|
Definition | df-cnp 13560* |
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 13561* |
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 | lmrcl 13562 |
Reverse closure for the convergence relation. (Contributed by Mario
Carneiro, 7-Sep-2015.)
|
⊢ (𝐹(⇝𝑡‘𝐽)𝑃 → 𝐽 ∈ Top) |
|
Theorem | lmfval 13563* |
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 | lmreltop 13564 |
The topological space convergence relation is a relation. (Contributed
by Jim Kingdon, 25-Mar-2023.)
|
⊢ (𝐽 ∈ Top → Rel
(⇝𝑡‘𝐽)) |
|
Theorem | cnfval 13565* |
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 13566* |
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 | cnovex 13567 |
The class of all continuous functions from a topology to another is a
set. (Contributed by Jim Kingdon, 14-Dec-2023.)
|
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 Cn 𝐾) ∈ V) |
|
Theorem | iscn 13568* |
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 13569* |
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 13570* |
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 13571* |
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 | cntop1 13572 |
Reverse closure for a continuous function. (Contributed by Mario
Carneiro, 21-Aug-2015.)
|
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) |
|
Theorem | cntop2 13573 |
Reverse closure for a continuous function. (Contributed by Mario
Carneiro, 21-Aug-2015.)
|
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
|
Theorem | iscnp3 13574* |
The predicate "the class 𝐹 is a continuous function from
topology
𝐽 to topology 𝐾 at point 𝑃".
(Contributed by NM,
15-May-2007.)
|
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ (◡𝐹 “ 𝑦)))))) |
|
Theorem | cnf 13575 |
A continuous function is a mapping. (Contributed by FL, 8-Dec-2006.)
(Revised by Mario Carneiro, 21-Aug-2015.)
|
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪
𝐾
⇒ ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶𝑌) |
|
Theorem | cnf2 13576 |
A continuous function is a mapping. (Contributed by Mario Carneiro,
21-Aug-2015.)
|
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌) |
|
Theorem | cnprcl2k 13577 |
Reverse closure for a function continuous at a point. (Contributed by
Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.)
|
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑃 ∈ 𝑋) |
|
Theorem | cnpf2 13578 |
A continuous function at point 𝑃 is a mapping. (Contributed by
Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.)
|
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋⟶𝑌) |
|
Theorem | tgcn 13579* |
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 13580* |
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 | ssidcn 13581 |
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 | icnpimaex 13582* |
Property of a function continuous at a point. (Contributed by FL,
31-Dec-2006.) (Revised by Jim Kingdon, 28-Mar-2023.)
|
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝐴)) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝐴)) |
|
Theorem | idcn 13583 |
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 13584* |
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 13561.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢)))) |
|
Theorem | lmbr2 13585* |
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 13586* |
Express the binary relation "sequence 𝐹 converges to point
𝑃 " in a metric space using an
arbitrary upper set of integers.
This version of lmbr2 13585 presupposes that 𝐹 is a function.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ 𝑍 =
(ℤ≥‘𝑀)
& ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋)
& ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝐴 ∈ 𝑢)))) |
|
Theorem | lmconst 13587 |
A constant sequence converges to its value. (Contributed by NM,
8-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
|
⊢ 𝑍 = (ℤ≥‘𝑀)
⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ) → (𝑍 × {𝑃})(⇝𝑡‘𝐽)𝑃) |
|
Theorem | lmcvg 13588* |
Convergence property of a converging sequence. (Contributed by Mario
Carneiro, 14-Nov-2013.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑃 ∈ 𝑈)
& ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)
& ⊢ (𝜑 → 𝑈 ∈ 𝐽) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑈) |
|
Theorem | iscnp4 13589* |
The predicate "the class 𝐹 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 13590* |
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 13591 |
An open subset of the codomain of a continuous function has an open
preimage. (Contributed by FL, 15-Dec-2006.)
|
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ 𝐾) → (◡𝐹 “ 𝐴) ∈ 𝐽) |
|
Theorem | cnco 13592 |
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 | cnptopco 13593 |
The composition of a function 𝐹 continuous at 𝑃 with a function
continuous at (𝐹‘𝑃) is continuous at 𝑃.
Proposition 2 of
[BourbakiTop1] p. I.9.
(Contributed by FL, 16-Nov-2006.) (Proof
shortened by Mario Carneiro, 27-Dec-2014.)
|
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)‘(𝐹‘𝑃)))) → (𝐺 ∘ 𝐹) ∈ ((𝐽 CnP 𝐿)‘𝑃)) |
|
Theorem | cnclima 13594 |
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 | cnntri 13595 |
Property of the preimage of an interior. (Contributed by Mario
Carneiro, 25-Aug-2015.)
|
⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 ⊆ 𝑌) → (◡𝐹 “ ((int‘𝐾)‘𝑆)) ⊆ ((int‘𝐽)‘(◡𝐹 “ 𝑆))) |
|
Theorem | cnntr 13596* |
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 13597 |
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 13598 |
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 13599 |
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 13600 |
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 𝐾)‘𝑃)) |