P. 228 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22701-22800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	metdstri 22701*	A generalization of the triangle inequality to the point-set distance function. Under the usual notation where the same symbol 𝑑 denotes the point-point and point-set distance functions, this theorem would be written 𝑑(𝑎, 𝑆) ≤ 𝑑(𝑎, 𝑏) + 𝑑(𝑏, 𝑆). (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    ⇒   ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ≤ ((𝐴𝐷𝐵) +𝑒 (𝐹‘𝐵)))
Theorem	metdsle 22702*	The distance from a point to a set is bounded by the distance to any member of the set. (Contributed by Mario Carneiro, 5-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    ⇒   ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐵) ≤ (𝐴𝐷𝐵))
Theorem	metdsre 22703*	The distance from a point to a nonempty set in a proper metric space is a real number. (Contributed by Mario Carneiro, 5-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    ⇒   ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → 𝐹:𝑋⟶ℝ)
Theorem	metdseq0 22704*	The distance from a point to a set is zero iff the point is in the closure set. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝐴) = 0 ↔ 𝐴 ∈ ((cls‘𝐽)‘𝑆)))
Theorem	metdscnlem 22705*	Lemma for metdscn 22706. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐶 = (dist‘ℝ*𝑠)    &   ⊢ 𝐾 = (MetOpen‘𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → (𝐴𝐷𝐵) < 𝑅)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐴) +𝑒 -𝑒(𝐹‘𝐵)) < 𝑅)
Theorem	metdscn 22706*	The function 𝐹 which gives the distance from a point to a set is a continuous function into the metric topology of the extended reals. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐶 = (dist‘ℝ*𝑠)    &   ⊢ 𝐾 = (MetOpen‘𝐶)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	metdscn2 22707*	The function 𝐹 which gives the distance from a point to a nonempty set in a metric space is a continuous function into the topology of the complex numbers. (Contributed by Mario Carneiro, 5-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	metnrmlem1a 22708*	Lemma for metnrm 22712. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → 𝑇 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → (0 < (𝐹‘𝐴) ∧ if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) ∈ ℝ+))
Theorem	metnrmlem1 22709*	Lemma for metnrm 22712. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → 𝑇 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → if(1 ≤ (𝐹‘𝐵), 1, (𝐹‘𝐵)) ≤ (𝐴𝐷𝐵))
Theorem	metnrmlem2 22710*	Lemma for metnrm 22712. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 5-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → 𝑇 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)    &   ⊢ 𝑈 = ∪ 𝑡 ∈ 𝑇 (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))    ⇒   ⊢ (𝜑 → (𝑈 ∈ 𝐽 ∧ 𝑇 ⊆ 𝑈))
Theorem	metnrmlem3 22711*	Lemma for metnrm 22712. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 5-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → 𝑇 ∈ (Clsd‘𝐽))    &   ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅)    &   ⊢ 𝑈 = ∪ 𝑡 ∈ 𝑇 (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))    &   ⊢ 𝐺 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑇 ↦ (𝑥𝐷𝑦)), ℝ*, < ))    &   ⊢ 𝑉 = ∪ 𝑠 ∈ 𝑆 (𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑆 ⊆ 𝑧 ∧ 𝑇 ⊆ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅))
Theorem	metnrm 22712	A metric space is normal. (Contributed by Jeff Hankins, 31-Aug-2013.) (Revised by Mario Carneiro, 5-Sep-2015.) (Proof shortened by AV, 30-Sep-2020.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Nrm)
Theorem	metreg 22713	A metric space is regular. (Contributed by Mario Carneiro, 29-Dec-2016.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Reg)
Theorem	addcnlem 22714*	Lemma for addcn 22715, subcn 22716, and mulcn 22717. (Contributed by Mario Carneiro, 5-May-2014.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ + :(ℂ × ℂ)⟶ℂ    &   ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝑏)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐))) < 𝑎))    ⇒   ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	addcn 22715	Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 30-Jul-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	subcn 22716	Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ − ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	mulcn 22717	Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 30-Jul-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ · ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	divcn 22718	Complex number division is a continuous function, when the second argument is nonzero. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t (ℂ ∖ {0}))    ⇒   ⊢ / ∈ ((𝐽 ×t 𝐾) Cn 𝐽)
Theorem	cnfldtgp 22719	The complex numbers form a topological group under addition, with the standard topology induced by the absolute value metric. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ ℂfld ∈ TopGrp
Theorem	fsumcn 22720*	A finite sum of functions to complex numbers from a common topological space is continuous. The class expression for 𝐵 normally contains free variables 𝑘 and 𝑥 to index it. (Contributed by NM, 8-Aug-2007.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn 𝐾))
Theorem	fsum2cn 22721*	Version of fsumcn 22720 for two-argument mappings. (Contributed by Mario Carneiro, 6-May-2014.)
⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑌))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐿) Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ ((𝐽 ×t 𝐿) Cn 𝐾))
Theorem	expcn 22722*	The power function on complex numbers, for fixed exponent 𝑁, is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (𝐽 Cn 𝐽))
Theorem	divccn 22723*	Division by a nonzero constant is a continuous operation. (Contributed by Mario Carneiro, 5-May-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 𝐴)) ∈ (𝐽 Cn 𝐽))
Theorem	sqcn 22724*	The square function on complex numbers is continuous. (Contributed by NM, 13-Jun-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ (𝐽 Cn 𝐽)
12.4.11  Topological definitions using the reals
Syntax	cii 22725	Extend class notation with the unit interval.
class II
Syntax	ccncf 22726	Extend class notation to include the operation which returns a class of continuous complex functions.
class –cn→
Definition	df-ii 22727	Define the unit interval with the Euclidean topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
⊢ II = (MetOpen‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))
Definition	df-cncf 22728*	Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.)
⊢ –cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏 ↑𝑚 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)})
Theorem	iitopon 22729	The unit interval is a topological space. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ II ∈ (TopOn‘(0[,]1))
Theorem	iitop 22730	The unit interval is a topological space. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ II ∈ Top
Theorem	iiuni 22731	The base set of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Jan-2014.)
⊢ (0[,]1) = ∪ II
Theorem	dfii2 22732	Alternate definition of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ II = ((topGen‘ran (,)) ↾t (0[,]1))
Theorem	dfii3 22733	Alternate definition of the unit interval. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ II = (𝐽 ↾t (0[,]1))
Theorem	dfii4 22734	Alternate definition of the unit interval. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐼 = (ℂfld ↾s (0[,]1))    ⇒   ⊢ II = (TopOpen‘𝐼)
Theorem	dfii5 22735	The unit interval expressed as an order topology. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ II = (ordTop‘( ≤ ∩ ((0[,]1) × (0[,]1))))
Theorem	iicmp 22736	The unit interval is compact. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Jun-2014.)
⊢ II ∈ Comp
Theorem	iiconn 22737	The unit interval is connected. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ II ∈ Conn
Theorem	cncfval 22738*	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 22739*	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 22740*	Version of elcncf 22739 with arguments commuted. (Contributed by Mario Carneiro, 28-Apr-2014.)
⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑦))))
Theorem	cncfrss 22741	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
Theorem	cncfrss2 22742	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
Theorem	cncff 22743	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 22744*	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 22745*	Membership in the set of continuous complex functions from 𝐴 to 𝐵. (Contributed by Paul Chapman, 26-Nov-2007.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+) → 𝑍 ∈ ℝ+))    &   ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ ℝ+) → ((abs‘(𝑥 − 𝑤)) < 𝑍 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))    ⇒   ⊢ (𝜑 → ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → 𝐹 ∈ (𝐴–cn→𝐵)))
Theorem	elcncf1ii 22746*	Membership in the set of continuous complex functions from 𝐴 to 𝐵. (Contributed by Paul Chapman, 26-Nov-2007.)
⊢ 𝐹:𝐴⟶𝐵    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+) → 𝑍 ∈ ℝ+)    &   ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ ℝ+) → ((abs‘(𝑥 − 𝑤)) < 𝑍 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))    ⇒   ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → 𝐹 ∈ (𝐴–cn→𝐵))
Theorem	rescncf 22747	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 22748	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 22749	The set of continuous functions is expanded when the range is expanded. (Contributed by Mario Carneiro, 30-Aug-2014.)
⊢ ((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ) → (𝐴–cn→𝐵) ⊆ (𝐴–cn→𝐶))
Theorem	climcncf 22750	Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵))    &   ⊢ (𝜑 → 𝐺:𝑍⟶𝐴)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺) ⇝ (𝐹‘𝐷))
Theorem	abscncf 22751	Absolute value is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ abs ∈ (ℂ–cn→ℝ)
Theorem	recncf 22752	Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ ℜ ∈ (ℂ–cn→ℝ)
Theorem	imcncf 22753	Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ ℑ ∈ (ℂ–cn→ℝ)
Theorem	cjcncf 22754	Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ ∗ ∈ (ℂ–cn→ℂ)
Theorem	mulc1cncf 22755*	Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	divccncf 22756*	Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 / 𝐴))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	cncfco 22757	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 22758	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	cncfcn 22759	Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝐴)    &   ⊢ 𝐿 = (𝐽 ↾t 𝐵)    ⇒   ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐴–cn→𝐵) = (𝐾 Cn 𝐿))
Theorem	cncfcn1 22760	Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (ℂ–cn→ℂ) = (𝐽 Cn 𝐽)
Theorem	cncfmptc 22761*	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 22762*	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 22763*	Composition of continuous functions. –cn→ analogue of cnmpt11f 21515. (Contributed by Mario Carneiro, 3-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐹‘𝐴)) ∈ (𝑋–cn→ℂ))
Theorem	cncfmpt2f 22764*	Composition of continuous functions. –cn→ analogue of cnmpt12f 21517. (Contributed by Mario Carneiro, 3-Sep-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	cncfmpt2ss 22765*	Composition of continuous functions in a subset. (Contributed by Mario Carneiro, 17-May-2016.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→𝑆))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→𝑆))    &   ⊢ 𝑆 ⊆ ℂ    &   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝑋–cn→𝑆))
Theorem	addccncf 22766*	Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 + 𝐴))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	cdivcncf 22767*	Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ ((ℂ ∖ {0})–cn→ℂ))
Theorem	negcncf 22768*	The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ -𝑥)    ⇒   ⊢ (𝐴 ⊆ ℂ → 𝐹 ∈ (𝐴–cn→ℂ))
Theorem	negfcncf 22769*	The negative of a continuous complex function is continuous. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ -(𝐹‘𝑥))    ⇒   ⊢ (𝐹 ∈ (𝐴–cn→ℂ) → 𝐺 ∈ (𝐴–cn→ℂ))
Theorem	abscncfALT 22770	Absolute value is continuous. Alternate proof of abscncf 22751. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ abs ∈ (ℂ–cn→ℝ)
Theorem	cncfcnvcn 22771	Rewrite cmphaushmeo 21651 for functions on the complex numbers. (Contributed by Mario Carneiro, 19-Feb-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝑋)    ⇒   ⊢ ((𝐾 ∈ Comp ∧ 𝐹 ∈ (𝑋–cn→𝑌)) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑌–cn→𝑋)))
Theorem	expcncf 22772*	The power function on complex numbers, for fixed exponent N, is continuous. Similar to expcn 22722. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (ℂ–cn→ℂ))
Theorem	cnmptre 22773*	Lemma for iirevcn 22776 and related functions. (Contributed by Mario Carneiro, 6-Jun-2014.)
⊢ 𝑅 = (TopOpen‘ℂfld)    &   ⊢ 𝐽 = ((topGen‘ran (,)) ↾t 𝐴)    &   ⊢ 𝐾 = ((topGen‘ran (,)) ↾t 𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝐹) ∈ (𝑅 Cn 𝑅))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐹) ∈ (𝐽 Cn 𝐾))
Theorem	cnmpt2pc 22774*	Piecewise definition of a continuous function on a real interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jun-2014.)
⊢ 𝑅 = (topGen‘ran (,))    &   ⊢ 𝑀 = (𝑅 ↾t (𝐴[,]𝐵))    &   ⊢ 𝑁 = (𝑅 ↾t (𝐵[,]𝐶))    &   ⊢ 𝑂 = (𝑅 ↾t (𝐴[,]𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐶))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐵 ∧ 𝑦 ∈ 𝑋)) → 𝐷 = 𝐸)    &   ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝑋 ↦ 𝐷) ∈ ((𝑀 ×t 𝐽) Cn 𝐾))    &   ⊢ (𝜑 → (𝑥 ∈ (𝐵[,]𝐶), 𝑦 ∈ 𝑋 ↦ 𝐸) ∈ ((𝑁 ×t 𝐽) Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) ∈ ((𝑂 ×t 𝐽) Cn 𝐾))
Theorem	iirev 22775	Reverse the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑋 ∈ (0[,]1) → (1 − 𝑋) ∈ (0[,]1))
Theorem	iirevcn 22776	The reversion function is a continuous map of the unit interval. (Contributed by Mario Carneiro, 6-Jun-2014.)
⊢ (𝑥 ∈ (0[,]1) ↦ (1 − 𝑥)) ∈ (II Cn II)
Theorem	iihalf1 22777	Map the first half of II into II. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑋 ∈ (0[,](1 / 2)) → (2 · 𝑋) ∈ (0[,]1))
Theorem	iihalf1cn 22778	The first half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.)
⊢ 𝐽 = ((topGen‘ran (,)) ↾t (0[,](1 / 2)))    ⇒   ⊢ (𝑥 ∈ (0[,](1 / 2)) ↦ (2 · 𝑥)) ∈ (𝐽 Cn II)
Theorem	iihalf2 22779	Map the second half of II into II. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑋 ∈ ((1 / 2)[,]1) → ((2 · 𝑋) − 1) ∈ (0[,]1))
Theorem	iihalf2cn 22780	The second half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.)
⊢ 𝐽 = ((topGen‘ran (,)) ↾t ((1 / 2)[,]1))    ⇒   ⊢ (𝑥 ∈ ((1 / 2)[,]1) ↦ ((2 · 𝑥) − 1)) ∈ (𝐽 Cn II)
Theorem	elii1 22781	Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.)
⊢ (𝑋 ∈ (0[,](1 / 2)) ↔ (𝑋 ∈ (0[,]1) ∧ 𝑋 ≤ (1 / 2)))
Theorem	elii2 22782	Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.)
⊢ ((𝑋 ∈ (0[,]1) ∧ ¬ 𝑋 ≤ (1 / 2)) → 𝑋 ∈ ((1 / 2)[,]1))
Theorem	iimulcl 22783	The unit interval is closed under multiplication. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐴 ∈ (0[,]1) ∧ 𝐵 ∈ (0[,]1)) → (𝐴 · 𝐵) ∈ (0[,]1))
Theorem	iimulcn 22784*	Multiplication is a continuous function on the unit interval. (Contributed by Mario Carneiro, 8-Jun-2014.)
⊢ (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑥 · 𝑦)) ∈ ((II ×t II) Cn II)
Theorem	icoopnst 22785	A half-open interval starting at 𝐴 is open in the closed interval from 𝐴 to 𝐵. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
⊢ 𝐽 = (MetOpen‘((abs ∘ − ) ↾ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴(,]𝐵) → (𝐴[,)𝐶) ∈ 𝐽))
Theorem	iocopnst 22786	A half-open interval ending at 𝐵 is open in the closed interval from 𝐴 to 𝐵. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
⊢ 𝐽 = (MetOpen‘((abs ∘ − ) ↾ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,)𝐵) → (𝐶(,]𝐵) ∈ 𝐽))
Theorem	icchmeo 22787*	The natural bijection from [0, 1] to an arbitrary nontrivial closed interval [𝐴, 𝐵] is a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹 ∈ (IIHomeo(𝐽 ↾t (𝐴[,]𝐵))))
Theorem	icopnfcnv 22788*	Define a bijection from [0, 1) to [0, +∞). (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))    ⇒   ⊢ (𝐹:(0[,)1)–1-1-onto→(0[,)+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,)+∞) ↦ (𝑦 / (1 + 𝑦))))
Theorem	icopnfhmeo 22789*	The defined bijection from [0, 1) to [0, +∞) is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥)))    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝐹 Isom < , < ((0[,)1), (0[,)+∞)) ∧ 𝐹 ∈ ((𝐽 ↾t (0[,)1))Homeo(𝐽 ↾t (0[,)+∞))))
Theorem	iccpnfcnv 22790*	Define a bijection from [0, 1] to [0, +∞]. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))))    ⇒   ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,]+∞) ↦ if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦)))))
Theorem	iccpnfhmeo 22791	The defined bijection from [0, 1] to [0, +∞] is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))))    &   ⊢ 𝐾 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))    ⇒   ⊢ (𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ 𝐹 ∈ (IIHomeo𝐾))
Theorem	xrhmeo 22792*	The bijection from [-1, 1] to the extended reals is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥))))    &   ⊢ 𝐺 = (𝑦 ∈ (-1[,]1) ↦ if(0 ≤ 𝑦, (𝐹‘𝑦), -𝑒(𝐹‘-𝑦)))    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (ordTop‘ ≤ )    ⇒   ⊢ (𝐺 Isom < , < ((-1[,]1), ℝ*) ∧ 𝐺 ∈ ((𝐽 ↾t (-1[,]1))Homeo(ordTop‘ ≤ )))
Theorem	xrhmph 22793	The extended reals are homeomorphic to the interval [0, 1]. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ II ≃ (ordTop‘ ≤ )
Theorem	xrcmp 22794	The topology of the extended reals is compact. Since the topology of the extended reals extends the topology of the reals (by xrtgioo 22656), this means that ℝ* is a compactification of ℝ. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (ordTop‘ ≤ ) ∈ Comp
Theorem	xrconn 22795	The topology of the extended reals is connected. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (ordTop‘ ≤ ) ∈ Conn
Theorem	icccvx 22796	A linear combination of two reals lies in the interval between them. Equivalently, a closed interval is a convex set. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐶 ∈ (𝐴[,]𝐵) ∧ 𝐷 ∈ (𝐴[,]𝐵) ∧ 𝑇 ∈ (0[,]1)) → (((1 − 𝑇) · 𝐶) + (𝑇 · 𝐷)) ∈ (𝐴[,]𝐵)))
Theorem	oprpiece1res1 22797*	Restriction to the first part of a piecewise defined function. (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof shortened by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐴 ≤ 𝐵    &   ⊢ 𝑅 ∈ V    &   ⊢ 𝑆 ∈ V    &   ⊢ 𝐾 ∈ (𝐴[,]𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝐶 ↦ if(𝑥 ≤ 𝐾, 𝑅, 𝑆))    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐾), 𝑦 ∈ 𝐶 ↦ 𝑅)    ⇒   ⊢ (𝐹 ↾ ((𝐴[,]𝐾) × 𝐶)) = 𝐺
Theorem	oprpiece1res2 22798*	Restriction to the second part of a piecewise defined function. (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof shortened by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐴 ≤ 𝐵    &   ⊢ 𝑅 ∈ V    &   ⊢ 𝑆 ∈ V    &   ⊢ 𝐾 ∈ (𝐴[,]𝐵)    &   ⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝐶 ↦ if(𝑥 ≤ 𝐾, 𝑅, 𝑆))    &   ⊢ (𝑥 = 𝐾 → 𝑅 = 𝑃)    &   ⊢ (𝑥 = 𝐾 → 𝑆 = 𝑄)    &   ⊢ (𝑦 ∈ 𝐶 → 𝑃 = 𝑄)    &   ⊢ 𝐺 = (𝑥 ∈ (𝐾[,]𝐵), 𝑦 ∈ 𝐶 ↦ 𝑆)    ⇒   ⊢ (𝐹 ↾ ((𝐾[,]𝐵) × 𝐶)) = 𝐺
Theorem	cnrehmeo 22799*	The canonical bijection from (ℝ × ℝ) to ℂ described in cnref1o 11865 is in fact a homeomorphism of the usual topologies on these sets. (It is also an isometry, if (ℝ × ℝ) is metrized with the l<SUP>2</SUP> norm.) (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐹 ∈ ((𝐽 ×t 𝐽)Homeo𝐾)
Theorem	cnheiborlem 22800*	Lemma for cnheibor 22801. (Contributed by Mario Carneiro, 14-Sep-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑇 = (𝐽 ↾t 𝑋)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    &   ⊢ 𝑌 = (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))    ⇒   ⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑇 ∈ Comp)