Theorem List for Intuitionistic Logic Explorer - 12401-12500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | mstri 12401 |
Triangle inequality for the distance function of a metric space.
Definition 14-1.1(d) of [Gleason] p.
223. (Contributed by Mario
Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐶𝐷𝐵))) |
|
Theorem | xmstri3 12402 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐵𝐷𝐶))) |
|
Theorem | mstri3 12403 |
Triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐵𝐷𝐶))) |
|
Theorem | msrtri 12404 |
Reverse triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 4-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘((𝐴𝐷𝐶) − (𝐵𝐷𝐶))) ≤ (𝐴𝐷𝐵)) |
|
Theorem | xmspropd 12405 |
Property deduction for an extended metric space. (Contributed by Mario
Carneiro, 4-Oct-2015.)
|
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))
⇒ ⊢ (𝜑 → (𝐾 ∈ ∞MetSp ↔ 𝐿 ∈
∞MetSp)) |
|
Theorem | mspropd 12406 |
Property deduction for a metric space. (Contributed by Mario Carneiro,
4-Oct-2015.)
|
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))
⇒ ⊢ (𝜑 → (𝐾 ∈ MetSp ↔ 𝐿 ∈ MetSp)) |
|
Theorem | setsmsbasg 12407 |
The base set of a constructed metric space. (Contributed by Mario
Carneiro, 28-Aug-2015.)
|
⊢ (𝜑 → 𝑋 = (Base‘𝑀)) & ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))) & ⊢ (𝜑 → 𝐾 = (𝑀 sSet 〈(TopSet‘ndx),
(MetOpen‘𝐷)〉)) & ⊢ (𝜑 → 𝑀 ∈ 𝑉)
& ⊢ (𝜑 → (MetOpen‘𝐷) ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑋 = (Base‘𝐾)) |
|
Theorem | setsmsdsg 12408 |
The distance function of a constructed metric space. (Contributed by
Mario Carneiro, 28-Aug-2015.)
|
⊢ (𝜑 → 𝑋 = (Base‘𝑀)) & ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))) & ⊢ (𝜑 → 𝐾 = (𝑀 sSet 〈(TopSet‘ndx),
(MetOpen‘𝐷)〉)) & ⊢ (𝜑 → 𝑀 ∈ 𝑉)
& ⊢ (𝜑 → (MetOpen‘𝐷) ∈ 𝑊) ⇒ ⊢ (𝜑 → (dist‘𝑀) = (dist‘𝐾)) |
|
Theorem | setsmstsetg 12409 |
The topology of a constructed metric space. (Contributed by Mario
Carneiro, 28-Aug-2015.) (Revised by Jim Kingdon, 7-May-2023.)
|
⊢ (𝜑 → 𝑋 = (Base‘𝑀)) & ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))) & ⊢ (𝜑 → 𝐾 = (𝑀 sSet 〈(TopSet‘ndx),
(MetOpen‘𝐷)〉)) & ⊢ (𝜑 → 𝑀 ∈ 𝑉)
& ⊢ (𝜑 → (MetOpen‘𝐷) ∈ 𝑊) ⇒ ⊢ (𝜑 → (MetOpen‘𝐷) = (TopSet‘𝐾)) |
|
Theorem | mopni 12410* |
An open set of a metric space includes a ball around each of its points.
(Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro,
12-Nov-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴) → ∃𝑥 ∈ ran (ball‘𝐷)(𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴)) |
|
Theorem | mopni2 12411* |
An open set of a metric space includes a ball around each of its points.
(Contributed by NM, 2-May-2007.) (Revised by Mario Carneiro,
12-Nov-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴) → ∃𝑥 ∈ ℝ+ (𝑃(ball‘𝐷)𝑥) ⊆ 𝐴) |
|
Theorem | mopni3 12412* |
An open set of a metric space includes an arbitrarily small ball around
each of its points. (Contributed by NM, 20-Sep-2007.) (Revised by
Mario Carneiro, 12-Nov-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴) ∧ 𝑅 ∈ ℝ+) →
∃𝑥 ∈
ℝ+ (𝑥
< 𝑅 ∧ (𝑃(ball‘𝐷)𝑥) ⊆ 𝐴)) |
|
Theorem | blssopn 12413 |
The balls of a metric space are open sets. (Contributed by NM,
12-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → ran (ball‘𝐷) ⊆ 𝐽) |
|
Theorem | unimopn 12414 |
The union of a collection of open sets of a metric space is open.
Theorem T2 of [Kreyszig] p. 19.
(Contributed by NM, 4-Sep-2006.)
(Revised by Mario Carneiro, 23-Dec-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ⊆ 𝐽) → ∪ 𝐴 ∈ 𝐽) |
|
Theorem | mopnin 12415 |
The intersection of two open sets of a metric space is open.
(Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro,
23-Dec-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽) |
|
Theorem | mopn0 12416 |
The empty set is an open set of a metric space. Part of Theorem T1 of
[Kreyszig] p. 19. (Contributed by NM,
4-Sep-2006.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → ∅ ∈ 𝐽) |
|
Theorem | rnblopn 12417 |
A ball of a metric space is an open set. (Contributed by NM,
12-Sep-2006.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ ran (ball‘𝐷)) → 𝐵 ∈ 𝐽) |
|
Theorem | blopn 12418 |
A ball of a metric space is an open set. (Contributed by NM,
9-Mar-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ∈ 𝐽) |
|
Theorem | neibl 12419* |
The neighborhoods around a point 𝑃 of a metric space are those
subsets containing a ball around 𝑃. Definition of neighborhood in
[Kreyszig] p. 19. (Contributed by NM,
8-Nov-2007.) (Revised by Mario
Carneiro, 23-Dec-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ 𝑋 ∧ ∃𝑟 ∈ ℝ+ (𝑃(ball‘𝐷)𝑟) ⊆ 𝑁))) |
|
Theorem | blnei 12420 |
A ball around a point is a neighborhood of the point. (Contributed by
NM, 8-Nov-2007.) (Revised by Mario Carneiro, 24-Aug-2015.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) ∈ ((nei‘𝐽)‘{𝑃})) |
|
Theorem | blsscls2 12421* |
A smaller closed ball is contained in a larger open ball. (Contributed
by Mario Carneiro, 10-Jan-2014.)
|
⊢ 𝐽 = (MetOpen‘𝐷)
& ⊢ 𝑆 = {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⇒ ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑇 ∈ ℝ*
∧ 𝑅 < 𝑇)) → 𝑆 ⊆ (𝑃(ball‘𝐷)𝑇)) |
|
Theorem | metss 12422* |
Two ways of saying that metric 𝐷 generates a finer topology than
metric 𝐶. (Contributed by Mario Carneiro,
12-Nov-2013.) (Revised
by Mario Carneiro, 24-Aug-2015.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (𝐽 ⊆ 𝐾 ↔ ∀𝑥 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟))) |
|
Theorem | metequiv 12423* |
Two ways of saying that two metrics generate the same topology. Two
metrics satisfying the right-hand side are said to be (topologically)
equivalent. (Contributed by Jeff Hankins, 21-Jun-2009.) (Revised by
Mario Carneiro, 12-Nov-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (𝐽 = 𝐾 ↔ ∀𝑥 ∈ 𝑋 (∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ ∀𝑎 ∈ ℝ+ ∃𝑏 ∈ ℝ+
(𝑥(ball‘𝐶)𝑏) ⊆ (𝑥(ball‘𝐷)𝑎)))) |
|
Theorem | metequiv2 12424* |
If there is a sequence of radii approaching zero for which the balls of
both metrics coincide, then the generated topologies are equivalent.
(Contributed by Mario Carneiro, 26-Aug-2015.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (∀𝑥 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+
(𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)) → 𝐽 = 𝐾)) |
|
Theorem | metss2lem 12425* |
Lemma for metss2 12426. (Contributed by Mario Carneiro,
14-Sep-2015.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷)
& ⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑥(ball‘𝐷)(𝑆 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑆)) |
|
Theorem | metss2 12426* |
If the metric 𝐷 is "strongly finer" than
𝐶
(meaning that there
is a positive real constant 𝑅 such that
𝐶(𝑥, 𝑦) ≤ 𝑅 · 𝐷(𝑥, 𝑦)), then 𝐷 generates a finer
topology. (Using this theorem twice in each direction states that if
two metrics are strongly equivalent, then they generate the same
topology.) (Contributed by Mario Carneiro, 14-Sep-2015.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷)
& ⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦))) ⇒ ⊢ (𝜑 → 𝐽 ⊆ 𝐾) |
|
Theorem | comet 12427* |
The composition of an extended metric with a monotonic subadditive
function is an extended metric. (Contributed by Mario Carneiro,
21-Mar-2015.)
|
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝐹:(0[,]+∞)⟶ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞)) → ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0))
& ⊢ ((𝜑
∧ (𝑥 ∈ (0[,]+∞) ∧
𝑦 ∈ (0[,]+∞))) →
(𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)))
& ⊢ ((𝜑
∧ (𝑥 ∈ (0[,]+∞) ∧
𝑦 ∈ (0[,]+∞))) →
(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦))) ⇒ ⊢ (𝜑
→ (𝐹 ∘ 𝐷) ∈ (∞Met‘𝑋)) |
|
Theorem | bdmetval 12428* |
Value of the standard bounded metric. (Contributed by Mario Carneiro,
26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.)
|
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, <
)) ⇒ ⊢ (((𝐶:(𝑋 × 𝑋)⟶ℝ* ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) = inf({(𝐴𝐶𝐵), 𝑅}, ℝ*, <
)) |
|
Theorem | bdxmet 12429* |
The standard bounded metric is an extended metric given an extended
metric and a positive extended real cutoff. (Contributed by Mario
Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.)
|
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, <
)) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐷 ∈ (∞Met‘𝑋)) |
|
Theorem | bdmet 12430* |
The standard bounded metric is a proper metric given an extended metric
and a positive real cutoff. (Contributed by Mario Carneiro,
26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.)
|
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, <
)) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ+) → 𝐷 ∈ (Met‘𝑋)) |
|
Theorem | bdbl 12431* |
The standard bounded metric corresponding to 𝐶 generates the same
balls as 𝐶 for radii less than 𝑅.
(Contributed by Mario
Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.)
|
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, <
)) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ* ∧ 𝑆 ≤ 𝑅)) → (𝑃(ball‘𝐷)𝑆) = (𝑃(ball‘𝐶)𝑆)) |
|
Theorem | bdmopn 12432* |
The standard bounded metric corresponding to 𝐶 generates the same
topology as 𝐶. (Contributed by Mario Carneiro,
26-Aug-2015.)
(Revised by Jim Kingdon, 19-May-2023.)
|
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, < )) & ⊢ 𝐽 = (MetOpen‘𝐶)
⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐽 = (MetOpen‘𝐷)) |
|
Theorem | mopnex 12433* |
The topology generated by an extended metric can also be generated by a
true metric. Thus, "metrizable topologies" can equivalently
be defined
in terms of metrics or extended metrics. (Contributed by Mario
Carneiro, 26-Aug-2015.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → ∃𝑑 ∈ (Met‘𝑋)𝐽 = (MetOpen‘𝑑)) |
|
Theorem | metrest 12434 |
Two alternate formulations of a subspace topology of a metric space
topology. (Contributed by Jeff Hankins, 19-Aug-2009.) (Proof shortened
by Mario Carneiro, 5-Jan-2014.)
|
⊢ 𝐷 = (𝐶 ↾ (𝑌 × 𝑌)) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷)
⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾t 𝑌) = 𝐾) |
|
6.2.5 Continuity in metric spaces
|
|
Theorem | metcnp3 12435* |
Two ways to express that 𝐹 is continuous at 𝑃 for
metric spaces.
Proposition 14-4.2 of [Gleason] p. 240.
(Contributed by NM,
17-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
(𝐹 “ (𝑃(ball‘𝐶)𝑧)) ⊆ ((𝐹‘𝑃)(ball‘𝐷)𝑦)))) |
|
Theorem | metcnp 12436* |
Two ways to say a mapping from metric 𝐶 to metric 𝐷 is
continuous at point 𝑃. (Contributed by NM, 11-May-2007.)
(Revised
by Mario Carneiro, 28-Aug-2015.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝑋 ((𝑃𝐶𝑤) < 𝑧 → ((𝐹‘𝑃)𝐷(𝐹‘𝑤)) < 𝑦)))) |
|
Theorem | metcnp2 12437* |
Two ways to say a mapping from metric 𝐶 to metric 𝐷 is
continuous at point 𝑃. The distance arguments are swapped
compared
to metcnp 12436 (and Munkres' metcn 12438) for compatibility with df-lm 12141.
Definition 1.3-3 of [Kreyszig] p. 20.
(Contributed by NM, 4-Jun-2007.)
(Revised by Mario Carneiro, 13-Nov-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝑋 ((𝑤𝐶𝑃) < 𝑧 → ((𝐹‘𝑤)𝐷(𝐹‘𝑃)) < 𝑦)))) |
|
Theorem | metcn 12438* |
Two ways to say a mapping from metric 𝐶 to metric 𝐷 is
continuous. Theorem 10.1 of [Munkres]
p. 127. The second biconditional
argument says that for every positive "epsilon" 𝑦 there
is a
positive "delta" 𝑧 such that a distance less than delta
in 𝐶
maps to a distance less than epsilon in 𝐷. (Contributed by NM,
15-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝐹‘𝑥)𝐷(𝐹‘𝑤)) < 𝑦)))) |
|
Theorem | metcnpi 12439* |
Epsilon-delta property of a continuous metric space function, with
function arguments as in metcnp 12436. (Contributed by NM, 17-Dec-2007.)
(Revised by Mario Carneiro, 13-Nov-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) →
∃𝑥 ∈
ℝ+ ∀𝑦 ∈ 𝑋 ((𝑃𝐶𝑦) < 𝑥 → ((𝐹‘𝑃)𝐷(𝐹‘𝑦)) < 𝐴)) |
|
Theorem | metcnpi2 12440* |
Epsilon-delta property of a continuous metric space function, with
swapped distance function arguments as in metcnp2 12437. (Contributed by
NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) →
∃𝑥 ∈
ℝ+ ∀𝑦 ∈ 𝑋 ((𝑦𝐶𝑃) < 𝑥 → ((𝐹‘𝑦)𝐷(𝐹‘𝑃)) < 𝐴)) |
|
Theorem | metcnpi3 12441* |
Epsilon-delta property of a metric space function continuous at 𝑃.
A variation of metcnpi2 12440 with non-strict ordering. (Contributed by
NM,
16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) →
∃𝑥 ∈
ℝ+ ∀𝑦 ∈ 𝑋 ((𝑦𝐶𝑃) ≤ 𝑥 → ((𝐹‘𝑦)𝐷(𝐹‘𝑃)) ≤ 𝐴)) |
|
Theorem | metcnpd 12442* |
Two ways to say a mapping from metric 𝐶 to metric 𝐷 is
continuous at point 𝑃. (Contributed by Jim Kingdon,
14-Jun-2023.)
|
⊢ (𝜑 → 𝐽 = (MetOpen‘𝐶)) & ⊢ (𝜑 → 𝐾 = (MetOpen‘𝐷)) & ⊢ (𝜑 → 𝐶 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑌)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝑋 ((𝑃𝐶𝑤) < 𝑧 → ((𝐹‘𝑃)𝐷(𝐹‘𝑤)) < 𝑦)))) |
|
6.2.6 Topology on the reals
|
|
Theorem | qtopbasss 12443* |
The set of open intervals with endpoints in a subset forms a basis for a
topology. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by
Jim Kingdon, 22-May-2023.)
|
⊢ 𝑆 ⊆ ℝ* & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → sup({𝑥, 𝑦}, ℝ*, < ) ∈ 𝑆) & ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → inf({𝑥, 𝑦}, ℝ*, < ) ∈ 𝑆)
⇒ ⊢ ((,) “ (𝑆 × 𝑆)) ∈ TopBases |
|
Theorem | qtopbas 12444 |
The set of open intervals with rational endpoints forms a basis for a
topology. (Contributed by NM, 8-Mar-2007.)
|
⊢ ((,) “ (ℚ × ℚ))
∈ TopBases |
|
Theorem | retopbas 12445 |
A basis for the standard topology on the reals. (Contributed by NM,
6-Feb-2007.) (Proof shortened by Mario Carneiro, 17-Jun-2014.)
|
⊢ ran (,) ∈ TopBases |
|
Theorem | retop 12446 |
The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
|
⊢ (topGen‘ran (,)) ∈
Top |
|
Theorem | uniretop 12447 |
The underlying set of the standard topology on the reals is the reals.
(Contributed by FL, 4-Jun-2007.)
|
⊢ ℝ = ∪
(topGen‘ran (,)) |
|
Theorem | retopon 12448 |
The standard topology on the reals is a topology on the reals.
(Contributed by Mario Carneiro, 28-Aug-2015.)
|
⊢ (topGen‘ran (,)) ∈
(TopOn‘ℝ) |
|
Theorem | retps 12449 |
The standard topological space on the reals. (Contributed by NM,
19-Oct-2012.)
|
⊢ 𝐾 = {〈(Base‘ndx), ℝ〉,
〈(TopSet‘ndx), (topGen‘ran
(,))〉} ⇒ ⊢ 𝐾 ∈ TopSp |
|
Theorem | iooretopg 12450 |
Open intervals are open sets of the standard topology on the reals .
(Contributed by FL, 18-Jun-2007.) (Revised by Jim Kingdon,
23-May-2023.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴(,)𝐵) ∈ (topGen‘ran
(,))) |
|
Theorem | cnmetdval 12451 |
Value of the distance function of the metric space of complex numbers.
(Contributed by NM, 9-Dec-2006.) (Revised by Mario Carneiro,
27-Dec-2014.)
|
⊢ 𝐷 = (abs ∘ −
) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵))) |
|
Theorem | cnmet 12452 |
The absolute value metric determines a metric space on the complex
numbers. This theorem provides a link between complex numbers and
metrics spaces, making metric space theorems available for use with
complex numbers. (Contributed by FL, 9-Oct-2006.)
|
⊢ (abs ∘ − ) ∈
(Met‘ℂ) |
|
Theorem | cnxmet 12453 |
The absolute value metric is an extended metric. (Contributed by Mario
Carneiro, 28-Aug-2015.)
|
⊢ (abs ∘ − ) ∈
(∞Met‘ℂ) |
|
Theorem | cntoptopon 12454 |
The topology of the complex numbers is a topology. (Contributed by Jim
Kingdon, 6-Jun-2023.)
|
⊢ 𝐽 = (MetOpen‘(abs ∘ −
)) ⇒ ⊢ 𝐽 ∈
(TopOn‘ℂ) |
|
Theorem | cntoptop 12455 |
The topology of the complex numbers is a topology. (Contributed by Jim
Kingdon, 6-Jun-2023.)
|
⊢ 𝐽 = (MetOpen‘(abs ∘ −
)) ⇒ ⊢ 𝐽 ∈ Top |
|
Theorem | cnbl0 12456 |
Two ways to write the open ball centered at zero. (Contributed by Mario
Carneiro, 8-Sep-2015.)
|
⊢ 𝐷 = (abs ∘ −
) ⇒ ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,)𝑅)) = (0(ball‘𝐷)𝑅)) |
|
Theorem | cnblcld 12457* |
Two ways to write the closed ball centered at zero. (Contributed by
Mario Carneiro, 8-Sep-2015.)
|
⊢ 𝐷 = (abs ∘ −
) ⇒ ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,]𝑅)) = {𝑥 ∈ ℂ ∣ (0𝐷𝑥) ≤ 𝑅}) |
|
Theorem | remetdval 12458 |
Value of the distance function of the metric space of real numbers.
(Contributed by NM, 16-May-2007.)
|
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ
× ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵))) |
|
Theorem | remet 12459 |
The absolute value metric determines a metric space on the reals.
(Contributed by NM, 10-Feb-2007.)
|
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ
× ℝ)) ⇒ ⊢ 𝐷 ∈
(Met‘ℝ) |
|
Theorem | rexmet 12460 |
The absolute value metric is an extended metric. (Contributed by Mario
Carneiro, 28-Aug-2015.)
|
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ
× ℝ)) ⇒ ⊢ 𝐷 ∈
(∞Met‘ℝ) |
|
Theorem | bl2ioo 12461 |
A ball in terms of an open interval of reals. (Contributed by NM,
18-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ
× ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(ball‘𝐷)𝐵) = ((𝐴 − 𝐵)(,)(𝐴 + 𝐵))) |
|
Theorem | ioo2bl 12462 |
An open interval of reals in terms of a ball. (Contributed by NM,
18-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ
× ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) = (((𝐴 + 𝐵) / 2)(ball‘𝐷)((𝐵 − 𝐴) / 2))) |
|
Theorem | ioo2blex 12463 |
An open interval of reals in terms of a ball. (Contributed by Mario
Carneiro, 14-Nov-2013.)
|
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ
× ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) ∈ ran (ball‘𝐷)) |
|
Theorem | blssioo 12464 |
The balls of the standard real metric space are included in the open
real intervals. (Contributed by NM, 8-May-2007.) (Revised by Mario
Carneiro, 13-Nov-2013.)
|
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ
× ℝ)) ⇒ ⊢ ran (ball‘𝐷) ⊆ ran
(,) |
|
Theorem | tgioo 12465 |
The topology generated by open intervals of reals is the same as the
open sets of the standard metric space on the reals. (Contributed by
NM, 7-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ
× ℝ))
& ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (topGen‘ran (,)) = 𝐽 |
|
Theorem | tgqioo 12466 |
The topology generated by open intervals of reals with rational
endpoints is the same as the open sets of the standard metric space on
the reals. In particular, this proves that the standard topology on the
reals is second-countable. (Contributed by Mario Carneiro,
17-Jun-2014.)
|
⊢ 𝑄 = (topGen‘((,) “ (ℚ
× ℚ))) ⇒ ⊢ (topGen‘ran (,)) = 𝑄 |
|
Theorem | resubmet 12467 |
The subspace topology induced by a subset of the reals. (Contributed by
Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Aug-2014.)
|
⊢ 𝑅 = (topGen‘ran (,)) & ⊢ 𝐽 = (MetOpen‘((abs ∘
− ) ↾ (𝐴
× 𝐴))) ⇒ ⊢ (𝐴 ⊆ ℝ → 𝐽 = (𝑅 ↾t 𝐴)) |
|
Theorem | tgioo2cntop 12468 |
The standard topology on the reals is a subspace of the complex metric
topology. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by
Jim Kingdon, 6-Aug-2023.)
|
⊢ 𝐽 = (MetOpen‘(abs ∘ −
)) ⇒ ⊢ (topGen‘ran (,)) = (𝐽 ↾t
ℝ) |
|
Theorem | rerestcntop 12469 |
The subspace topology induced by a subset of the reals. (Contributed by
Mario Carneiro, 13-Aug-2014.) (Revised by Jim Kingdon, 6-Aug-2023.)
|
⊢ 𝐽 = (MetOpen‘(abs ∘ −
))
& ⊢ 𝑅 = (topGen‘ran
(,)) ⇒ ⊢ (𝐴 ⊆ ℝ → (𝐽 ↾t 𝐴) = (𝑅 ↾t 𝐴)) |
|
6.2.7 Topological definitions using the
reals
|
|
Syntax | ccncf 12470 |
Extend class notation to include the operation which returns a class of
continuous complex functions.
|
class –cn→ |
|
Definition | df-cncf 12471* |
Define the operation whose value is a class of continuous complex
functions. (Contributed by Paul Chapman, 11-Oct-2007.)
|
⊢ –cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ
↦ {𝑓 ∈ (𝑏 ↑𝑚
𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)}) |
|
Theorem | cncfval 12472* |
The value of the continuous complex function operation is the set of
continuous functions from 𝐴 to 𝐵. (Contributed by Paul
Chapman, 11-Oct-2007.) (Revised by Mario Carneiro, 9-Nov-2013.)
|
⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐴–cn→𝐵) = {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑤))) < 𝑦)}) |
|
Theorem | elcncf 12473* |
Membership in the set of continuous complex functions from 𝐴 to
𝐵. (Contributed by Paul Chapman,
11-Oct-2007.) (Revised by Mario
Carneiro, 9-Nov-2013.)
|
⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))) |
|
Theorem | elcncf2 12474* |
Version of elcncf 12473 with arguments commuted. (Contributed by
Mario
Carneiro, 28-Apr-2014.)
|
⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑦)))) |
|
Theorem | cncfrss 12475 |
Reverse closure of the continuous function predicate. (Contributed by
Mario Carneiro, 25-Aug-2014.)
|
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ) |
|
Theorem | cncfrss2 12476 |
Reverse closure of the continuous function predicate. (Contributed by
Mario Carneiro, 25-Aug-2014.)
|
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ) |
|
Theorem | cncff 12477 |
A continuous complex function's domain and codomain. (Contributed by
Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro,
25-Aug-2014.)
|
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐹:𝐴⟶𝐵) |
|
Theorem | cncfi 12478* |
Defining property of a continuous function. (Contributed by Mario
Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.)
|
⊢ ((𝐹 ∈ (𝐴–cn→𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝑅 ∈ ℝ+) →
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝐶))) < 𝑅)) |
|
Theorem | elcncf1di 12479* |
Membership in the set of continuous complex functions from 𝐴 to
𝐵. (Contributed by Paul Chapman,
26-Nov-2007.)
|
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
& ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+) → 𝑍 ∈
ℝ+))
& ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ ℝ+) →
((abs‘(𝑥 −
𝑤)) < 𝑍 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))) ⇒ ⊢ (𝜑 → ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → 𝐹 ∈ (𝐴–cn→𝐵))) |
|
Theorem | elcncf1ii 12480* |
Membership in the set of continuous complex functions from 𝐴 to
𝐵. (Contributed by Paul Chapman,
26-Nov-2007.)
|
⊢ 𝐹:𝐴⟶𝐵
& ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+) → 𝑍 ∈
ℝ+)
& ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ ℝ+) →
((abs‘(𝑥 −
𝑤)) < 𝑍 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)) ⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → 𝐹 ∈ (𝐴–cn→𝐵)) |
|
Theorem | rescncf 12481 |
A continuous complex function restricted to a subset is continuous.
(Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro,
25-Aug-2014.)
|
⊢ (𝐶 ⊆ 𝐴 → (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹 ↾ 𝐶) ∈ (𝐶–cn→𝐵))) |
|
Theorem | cncffvrn 12482 |
Change the codomain of a continuous complex function. (Contributed by
Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 1-May-2015.)
|
⊢ ((𝐶 ⊆ ℂ ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → (𝐹 ∈ (𝐴–cn→𝐶) ↔ 𝐹:𝐴⟶𝐶)) |
|
Theorem | cncfss 12483 |
The set of continuous functions is expanded when the range is expanded.
(Contributed by Mario Carneiro, 30-Aug-2014.)
|
⊢ ((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ) → (𝐴–cn→𝐵) ⊆ (𝐴–cn→𝐶)) |
|
Theorem | climcncf 12484 |
Image of a limit under a continuous map. (Contributed by Mario
Carneiro, 7-Apr-2015.)
|
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵)) & ⊢ (𝜑 → 𝐺:𝑍⟶𝐴)
& ⊢ (𝜑 → 𝐺 ⇝ 𝐷)
& ⊢ (𝜑 → 𝐷 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺) ⇝ (𝐹‘𝐷)) |
|
Theorem | abscncf 12485 |
Absolute value is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
⊢ abs ∈ (ℂ–cn→ℝ) |
|
Theorem | recncf 12486 |
Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.)
(Revised by Mario Carneiro, 28-Apr-2014.)
|
⊢ ℜ ∈ (ℂ–cn→ℝ) |
|
Theorem | imcncf 12487 |
Imaginary part is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
⊢ ℑ ∈ (ℂ–cn→ℝ) |
|
Theorem | cjcncf 12488 |
Complex conjugate is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
⊢ ∗ ∈ (ℂ–cn→ℂ) |
|
Theorem | mulc1cncf 12489* |
Multiplication by a constant is continuous. (Contributed by Paul
Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) |
|
Theorem | divccncfap 12490* |
Division by a constant is continuous. (Contributed by Paul Chapman,
28-Nov-2007.) (Revised by Jim Kingdon, 9-Jan-2023.)
|
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 / 𝐴)) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → 𝐹 ∈ (ℂ–cn→ℂ)) |
|
Theorem | cncfco 12491 |
The composition of two continuous maps on complex numbers is also
continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by
Mario Carneiro, 25-Aug-2014.)
|
⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵)) & ⊢ (𝜑 → 𝐺 ∈ (𝐵–cn→𝐶)) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) ∈ (𝐴–cn→𝐶)) |
|
Theorem | cncfmet 12492 |
Relate complex function continuity to metric space continuity.
(Contributed by Paul Chapman, 26-Nov-2007.) (Revised by Mario Carneiro,
7-Sep-2015.)
|
⊢ 𝐶 = ((abs ∘ − ) ↾ (𝐴 × 𝐴)) & ⊢ 𝐷 = ((abs ∘ − )
↾ (𝐵 × 𝐵)) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷)
⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐴–cn→𝐵) = (𝐽 Cn 𝐾)) |
|
Theorem | cncfcncntop 12493 |
Relate complex function continuity to topological continuity.
(Contributed by Mario Carneiro, 17-Feb-2015.)
|
⊢ 𝐽 = (MetOpen‘(abs ∘ −
))
& ⊢ 𝐾 = (𝐽 ↾t 𝐴)
& ⊢ 𝐿 = (𝐽 ↾t 𝐵) ⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐴–cn→𝐵) = (𝐾 Cn 𝐿)) |
|
Theorem | cncfcn1cntop 12494 |
Relate complex function continuity to topological continuity.
(Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro,
7-Sep-2015.) (Revised by Jim Kingdon, 16-Jun-2023.)
|
⊢ 𝐽 = (MetOpen‘(abs ∘ −
)) ⇒ ⊢ (ℂ–cn→ℂ) = (𝐽 Cn 𝐽) |
|
Theorem | cncfmptc 12495* |
A constant function is a continuous function on ℂ. (Contributed
by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro,
7-Sep-2015.)
|
⊢ ((𝐴 ∈ 𝑇 ∧ 𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→𝑇)) |
|
Theorem | cncfmptid 12496* |
The identity function is a continuous function on ℂ. (Contributed
by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro,
17-May-2016.)
|
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (𝑥 ∈ 𝑆 ↦ 𝑥) ∈ (𝑆–cn→𝑇)) |
|
Theorem | cncfmpt1f 12497* |
Composition of continuous functions. –cn→ analogue of cnmpt11f 12234.
(Contributed by Mario Carneiro, 3-Sep-2014.)
|
⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐹‘𝐴)) ∈ (𝑋–cn→ℂ)) |
|
Theorem | addccncf 12498* |
Adding a constant is a continuous function. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 + 𝐴)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) |
|
Theorem | cdivcncfap 12499* |
Division with a constant numerator is continuous. (Contributed by Mario
Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 26-May-2023.)
|
⊢ 𝐹 = (𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (𝐴 / 𝑥)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ ({𝑦 ∈ ℂ ∣ 𝑦 # 0}–cn→ℂ)) |
|
Theorem | negcncf 12500* |
The negative function is continuous. (Contributed by Mario Carneiro,
30-Dec-2016.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ -𝑥) ⇒ ⊢ (𝐴 ⊆ ℂ → 𝐹 ∈ (𝐴–cn→ℂ)) |