P. 250 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24901-25000   *Has distinct variable group(s)

Type	Label	Description
Statement
12.4.11  Topological definitions using the reals
Syntax	cii 24901	Extend class notation with the unit interval.
class II
Syntax	ccncf 24902	Extend class notation to include the operation which returns a class of continuous complex functions.
class –cn→
Definition	df-ii 24903	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 24904*	Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.)
⊢ –cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏 ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)})
Theorem	iitopon 24905	The unit interval is a topological space. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ II ∈ (TopOn‘(0[,]1))
Theorem	iitop 24906	The unit interval is a topological space. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ II ∈ Top
Theorem	iiuni 24907	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 24908	Alternate definition of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ II = ((topGen‘ran (,)) ↾t (0[,]1))
Theorem	dfii3 24909	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 24910	Alternate definition of the unit interval. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐼 = (ℂfld ↾s (0[,]1))    ⇒   ⊢ II = (TopOpen‘𝐼)
Theorem	dfii5 24911	The unit interval expressed as an order topology. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ II = (ordTop‘( ≤ ∩ ((0[,]1) × (0[,]1))))
Theorem	iicmp 24912	The unit interval is compact. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Jun-2014.)
⊢ II ∈ Comp
Theorem	iiconn 24913	The unit interval is connected. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ II ∈ Conn
Theorem	cncfval 24914*	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→𝐵) = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑤))) < 𝑦)})
Theorem	elcncf 24915*	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 24916*	Version of elcncf 24915 with arguments commuted. (Contributed by Mario Carneiro, 28-Apr-2014.)
⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑦))))
Theorem	cncfrss 24917	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
Theorem	cncfrss2 24918	Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
Theorem	cncff 24919	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 24920*	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 24921*	Membership in the set of continuous complex functions from 𝐴 to 𝐵. (Contributed by Paul Chapman, 26-Nov-2007.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+) → 𝑍 ∈ ℝ+))    &   ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ ℝ+) → ((abs‘(𝑥 − 𝑤)) < 𝑍 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))    ⇒   ⊢ (𝜑 → ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → 𝐹 ∈ (𝐴–cn→𝐵)))
Theorem	elcncf1ii 24922*	Membership in the set of continuous complex functions from 𝐴 to 𝐵. (Contributed by Paul Chapman, 26-Nov-2007.)
⊢ 𝐹:𝐴⟶𝐵    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+) → 𝑍 ∈ ℝ+)    &   ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ ℝ+) → ((abs‘(𝑥 − 𝑤)) < 𝑍 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))    ⇒   ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → 𝐹 ∈ (𝐴–cn→𝐵))
Theorem	rescncf 24923	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	cncfcdm 24924	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 24925	The set of continuous functions is expanded when the codomain is expanded. (Contributed by Mario Carneiro, 30-Aug-2014.)
⊢ ((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ) → (𝐴–cn→𝐵) ⊆ (𝐴–cn→𝐶))
Theorem	climcncf 24926	Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵))    &   ⊢ (𝜑 → 𝐺:𝑍⟶𝐴)    &   ⊢ (𝜑 → 𝐺 ⇝ 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺) ⇝ (𝐹‘𝐷))
Theorem	abscncf 24927	Absolute value is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ abs ∈ (ℂ–cn→ℝ)
Theorem	recncf 24928	Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ ℜ ∈ (ℂ–cn→ℝ)
Theorem	imcncf 24929	Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ ℑ ∈ (ℂ–cn→ℝ)
Theorem	cjcncf 24930	Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
⊢ ∗ ∈ (ℂ–cn→ℂ)
Theorem	mulc1cncf 24931*	Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	divccncf 24932*	Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 / 𝐴))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	cncfco 24933	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	cncfcompt2 24934*	Composition of continuous functions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (𝐴–cn→𝐵))    &   ⊢ (𝜑 → (𝑦 ∈ 𝐶 ↦ 𝑆) ∈ (𝐶–cn→𝐸))    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    &   ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑇) ∈ (𝐴–cn→𝐸))
Theorem	cncfmet 24935	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 24936	Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝐴)    &   ⊢ 𝐿 = (𝐽 ↾t 𝐵)    ⇒   ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐴–cn→𝐵) = (𝐾 Cn 𝐿))
Theorem	cncfcn1 24937	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 24938*	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 24939*	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 24940*	Composition of continuous functions. –cn→ analogue of cnmpt11f 23672. (Contributed by Mario Carneiro, 3-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐹‘𝐴)) ∈ (𝑋–cn→ℂ))
Theorem	cncfmpt2f 24941*	Composition of continuous functions. –cn→ analogue of cnmpt12f 23674. (Contributed by Mario Carneiro, 3-Sep-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝑋–cn→ℂ))
Theorem	cncfmpt2ss 24942*	Composition of continuous functions in a subset. (Contributed by Mario Carneiro, 17-May-2016.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→𝑆))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→𝑆))    &   ⊢ 𝑆 ⊆ ℂ    &   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝑋–cn→𝑆))
Theorem	addccncf 24943*	Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 + 𝐴))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	idcncf 24944	The identity function is a continuous function on ℂ. (Contributed by Jeff Madsen, 11-Jun-2010.) (Moved into main set.mm as cncfmptid 24939 and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝑥)    ⇒   ⊢ 𝐹 ∈ (ℂ–cn→ℂ)
Theorem	sub1cncf 24945*	Subtracting a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 − 𝐴))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	sub2cncf 24946*	Subtraction from a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 − 𝑥))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ))
Theorem	cdivcncf 24947*	Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥))    ⇒   ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ ((ℂ ∖ {0})–cn→ℂ))
Theorem	negcncf 24948*	The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016.) Avoid ax-mulf 11235. (Revised by GG, 16-Mar-2025.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ -𝑥)    ⇒   ⊢ (𝐴 ⊆ ℂ → 𝐹 ∈ (𝐴–cn→ℂ))
Theorem	negcncfOLD 24949*	Obsolete version of negcncf 24948 as of 9-Apr-2025. (Contributed by Mario Carneiro, 30-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ -𝑥)    ⇒   ⊢ (𝐴 ⊆ ℂ → 𝐹 ∈ (𝐴–cn→ℂ))
Theorem	negfcncf 24950*	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 24951	Absolute value is continuous. Alternate proof of abscncf 24927. (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 24952	Rewrite cmphaushmeo 23808 for functions on the complex numbers. (Contributed by Mario Carneiro, 19-Feb-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝑋)    ⇒   ⊢ ((𝐾 ∈ Comp ∧ 𝐹 ∈ (𝑋–cn→𝑌)) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑌–cn→𝑋)))
Theorem	expcncf 24953*	The power function on complex numbers, for fixed exponent N, is continuous. Similar to expcn 24896. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (ℂ–cn→ℂ))
Theorem	cnmptre 24954*	Lemma for iirevcn 24957 and related functions. (Contributed by Mario Carneiro, 6-Jun-2014.)
⊢ 𝑅 = (TopOpen‘ℂfld)    &   ⊢ 𝐽 = ((topGen‘ran (,)) ↾t 𝐴)    &   ⊢ 𝐾 = ((topGen‘ran (,)) ↾t 𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝐹) ∈ (𝑅 Cn 𝑅))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐹) ∈ (𝐽 Cn 𝐾))
Theorem	cnmpopc 24955*	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 24956	Reverse the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑋 ∈ (0[,]1) → (1 − 𝑋) ∈ (0[,]1))
Theorem	iirevcn 24957	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 24958	Map the first half of II into II. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑋 ∈ (0[,](1 / 2)) → (2 · 𝑋) ∈ (0[,]1))
Theorem	iihalf1cn 24959	The first half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.) Avoid ax-mulf 11235. (Revised by GG, 16-Mar-2025.)
⊢ 𝐽 = ((topGen‘ran (,)) ↾t (0[,](1 / 2)))    ⇒   ⊢ (𝑥 ∈ (0[,](1 / 2)) ↦ (2 · 𝑥)) ∈ (𝐽 Cn II)
Theorem	iihalf1cnOLD 24960	Obsolete version of iihalf1cn 24959 as of 9-Apr-2025. (Contributed by Mario Carneiro, 6-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐽 = ((topGen‘ran (,)) ↾t (0[,](1 / 2)))    ⇒   ⊢ (𝑥 ∈ (0[,](1 / 2)) ↦ (2 · 𝑥)) ∈ (𝐽 Cn II)
Theorem	iihalf2 24961	Map the second half of II into II. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑋 ∈ ((1 / 2)[,]1) → ((2 · 𝑋) − 1) ∈ (0[,]1))
Theorem	iihalf2cn 24962	The second half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.) Avoid ax-mulf 11235. (Revised by GG, 16-Mar-2025.)
⊢ 𝐽 = ((topGen‘ran (,)) ↾t ((1 / 2)[,]1))    ⇒   ⊢ (𝑥 ∈ ((1 / 2)[,]1) ↦ ((2 · 𝑥) − 1)) ∈ (𝐽 Cn II)
Theorem	iihalf2cnOLD 24963	Obsolete version of iihalf2cn 24962 as of 9-Apr-2025. (Contributed by Mario Carneiro, 6-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐽 = ((topGen‘ran (,)) ↾t ((1 / 2)[,]1))    ⇒   ⊢ (𝑥 ∈ ((1 / 2)[,]1) ↦ ((2 · 𝑥) − 1)) ∈ (𝐽 Cn II)
Theorem	elii1 24964	Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.)
⊢ (𝑋 ∈ (0[,](1 / 2)) ↔ (𝑋 ∈ (0[,]1) ∧ 𝑋 ≤ (1 / 2)))
Theorem	elii2 24965	Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.)
⊢ ((𝑋 ∈ (0[,]1) ∧ ¬ 𝑋 ≤ (1 / 2)) → 𝑋 ∈ ((1 / 2)[,]1))
Theorem	iimulcl 24966	The unit interval is closed under multiplication. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐴 ∈ (0[,]1) ∧ 𝐵 ∈ (0[,]1)) → (𝐴 · 𝐵) ∈ (0[,]1))
Theorem	iimulcn 24967*	Multiplication is a continuous function on the unit interval. (Contributed by Mario Carneiro, 8-Jun-2014.) Avoid ax-mulf 11235. (Revised by GG, 16-Mar-2025.)
⊢ (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑥 · 𝑦)) ∈ ((II ×t II) Cn II)
Theorem	iimulcnOLD 24968*	Obsolete version of iimulcn 24967 as of 9-Apr-2025. (Contributed by Mario Carneiro, 8-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑥 · 𝑦)) ∈ ((II ×t II) Cn II)
Theorem	icoopnst 24969	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 24970	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 24971*	The natural bijection from [0, 1] to an arbitrary nontrivial closed interval [𝐴, 𝐵] is a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015.) Avoid ax-mulf 11235. (Revised by GG, 16-Mar-2025.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹 ∈ (IIHomeo(𝐽 ↾t (𝐴[,]𝐵))))
Theorem	icchmeoOLD 24972*	Obsolete version of icchmeo 24971 as of 9-Apr-2025. (Contributed by Mario Carneiro, 8-Sep-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴)))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹 ∈ (IIHomeo(𝐽 ↾t (𝐴[,]𝐵))))
Theorem	icopnfcnv 24973*	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 24974*	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 24975*	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 24976	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 24977*	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)    ⇒   ⊢ (𝐺 Isom < , < ((-1[,]1), ℝ*) ∧ 𝐺 ∈ ((𝐽 ↾t (-1[,]1))Homeo(ordTop‘ ≤ )))
Theorem	xrhmph 24978	The extended reals are homeomorphic to the interval [0, 1]. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ II ≃ (ordTop‘ ≤ )
Theorem	xrcmp 24979	The topology of the extended reals is compact. Since the topology of the extended reals extends the topology of the reals (by xrtgioo 24828), this means that ℝ* is a compactification of ℝ. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (ordTop‘ ≤ ) ∈ Comp
Theorem	xrconn 24980	The topology of the extended reals is connected. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (ordTop‘ ≤ ) ∈ Conn
Theorem	icccvx 24981	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 24982*	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 24983*	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 24984*	The canonical bijection from (ℝ × ℝ) to ℂ described in cnref1o 13027 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.) Avoid ax-mulf 11235. (Revised by GG, 16-Mar-2025.)
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐹 ∈ ((𝐽 ×t 𝐽)Homeo𝐾)
Theorem	cnrehmeoOLD 24985*	Obsolete version of cnrehmeo 24984 as of 9-Apr-2025. (Contributed by Mario Carneiro, 25-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐹 ∈ ((𝐽 ×t 𝐽)Homeo𝐾)
Theorem	cnheiborlem 24986*	Lemma for cnheibor 24987. (Contributed by Mario Carneiro, 14-Sep-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑇 = (𝐽 ↾t 𝑋)    &   ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    &   ⊢ 𝑌 = (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅)))    ⇒   ⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑇 ∈ Comp)
Theorem	cnheibor 24987*	Heine-Borel theorem for complex numbers. A subset of ℂ is compact iff it is closed and bounded. (Contributed by Mario Carneiro, 14-Sep-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑇 = (𝐽 ↾t 𝑋)    ⇒   ⊢ (𝑋 ⊆ ℂ → (𝑇 ∈ Comp ↔ (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟)))
Theorem	cnllycmp 24988	The topology on the complex numbers is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐽 ∈ 𝑛-Locally Comp
Theorem	rellycmp 24989	The topology on the reals is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (topGen‘ran (,)) ∈ 𝑛-Locally Comp
Theorem	bndth 24990*	The Boundedness Theorem. A continuous function from a compact topological space to the reals is bounded (above). (Boundedness below is obtained by applying this theorem to -𝐹.) (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ 𝑥)
Theorem	evth 24991*	The Extreme Value Theorem. A continuous function from a nonempty compact topological space to the reals attains its maximum at some point in the domain. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥))
Theorem	evth2 24992*	The Extreme Value Theorem, minimum version. A continuous function from a nonempty compact topological space to the reals attains its minimum at some point in the domain. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑥) ≤ (𝐹‘𝑦))
Theorem	lebnumlem1 24993*	Lemma for lebnum 24996. The function 𝐹 measures the sum of all of the distances to escape the sets of the cover. Since by assumption it is a cover, there is at least one set which covers a given point, and since it is open, the point is a positive distance from the edge of the set. Thus, the sum is a strictly positive number. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by AV, 30-Sep-2020.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    &   ⊢ 𝐹 = (𝑦 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))    ⇒   ⊢ (𝜑 → 𝐹:𝑋⟶ℝ+)
Theorem	lebnumlem2 24994*	Lemma for lebnum 24996. As a finite sum of point-to-set distance functions, which are continuous by metdscn 24878, the function 𝐹 is also continuous. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by AV, 30-Sep-2020.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    &   ⊢ 𝐹 = (𝑦 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))    &   ⊢ 𝐾 = (topGen‘ran (,))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))
Theorem	lebnumlem3 24995*	Lemma for lebnum 24996. By the previous lemmas, 𝐹 is continuous and positive on a compact set, so it has a positive minimum 𝑟. Then setting 𝑑 = 𝑟 / ♯(𝑈), since for each 𝑢 ∈ 𝑈 we have ball(𝑥, 𝑑) ⊆ 𝑢 iff 𝑑 ≤ 𝑑(𝑥, 𝑋 ∖ 𝑢), if ¬ ball(𝑥, 𝑑) ⊆ 𝑢 for all 𝑢 then summing over 𝑢 yields Σ𝑢 ∈ 𝑈𝑑(𝑥, 𝑋 ∖ 𝑢) = 𝐹(𝑥) < Σ𝑢 ∈ 𝑈𝑑 = 𝑟, in contradiction to the assumption that 𝑟 is the minimum of 𝐹. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.) (Revised by AV, 30-Sep-2020.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈)    &   ⊢ 𝐹 = (𝑦 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < ))    &   ⊢ 𝐾 = (topGen‘ran (,))    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)
Theorem	lebnum 24996*	The Lebesgue number lemma, or Lebesgue covering lemma. If 𝑋 is a compact metric space and 𝑈 is an open cover of 𝑋, then there exists a positive real number 𝑑 such that every ball of size 𝑑 (and every subset of a ball of size 𝑑, including every subset of diameter less than 𝑑) is a subset of some member of the cover. (Contributed by Mario Carneiro, 14-Feb-2015.) (Proof shortened by Mario Carneiro, 5-Sep-2015.) (Proof shortened by AV, 30-Sep-2020.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)
Theorem	xlebnum 24997*	Generalize lebnum 24996 to extended metrics. (Contributed by Mario Carneiro, 5-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝑈 ⊆ 𝐽)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝑈)    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)
Theorem	lebnumii 24998*	Specialize the Lebesgue number lemma lebnum 24996 to the closed unit interval. (Contributed by Mario Carneiro, 14-Feb-2015.)
⊢ ((𝑈 ⊆ II ∧ (0[,]1) = ∪ 𝑈) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑢 ∈ 𝑈 (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑢)
12.4.12  Path homotopy
Syntax	chtpy 24999	Extend class notation with the class of homotopies between two continuous functions.
class Htpy
Syntax	cphtpy 25000	Extend class notation with the class of path homotopies between two continuous functions.
class PHtpy