![]() |
Metamath
Proof Explorer Theorem List (p. 243 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nlmvscnlem2 24201 | Lemma for nlmvscn 24203. Compare this proof with the similar elementary proof mulcn2 15539 for continuity of multiplication on β. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ π = (Baseβπ) & β’ πΎ = (BaseβπΉ) & β’ π· = (distβπ) & β’ πΈ = (distβπΉ) & β’ π = (normβπ) & β’ π΄ = (normβπΉ) & β’ Β· = ( Β·π βπ) & β’ π = ((π / 2) / ((π΄βπ΅) + 1)) & β’ π = ((π / 2) / ((πβπ) + π)) & β’ (π β π β NrmMod) & β’ (π β π β β+) & β’ (π β π΅ β πΎ) & β’ (π β π β π) & β’ (π β πΆ β πΎ) & β’ (π β π β π) & β’ (π β (π΅πΈπΆ) < π) & β’ (π β (ππ·π) < π) β β’ (π β ((π΅ Β· π)π·(πΆ Β· π)) < π ) | ||
Theorem | nlmvscnlem1 24202* | Lemma for nlmvscn 24203. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ π = (Baseβπ) & β’ πΎ = (BaseβπΉ) & β’ π· = (distβπ) & β’ πΈ = (distβπΉ) & β’ π = (normβπ) & β’ π΄ = (normβπΉ) & β’ Β· = ( Β·π βπ) & β’ π = ((π / 2) / ((π΄βπ΅) + 1)) & β’ π = ((π / 2) / ((πβπ) + π)) & β’ (π β π β NrmMod) & β’ (π β π β β+) & β’ (π β π΅ β πΎ) & β’ (π β π β π) β β’ (π β βπ β β+ βπ₯ β πΎ βπ¦ β π (((π΅πΈπ₯) < π β§ (ππ·π¦) < π) β ((π΅ Β· π)π·(π₯ Β· π¦)) < π )) | ||
Theorem | nlmvscn 24203 | The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 24206 and nlmtlm 24210. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·sf βπ) & β’ π½ = (TopOpenβπ) & β’ πΎ = (TopOpenβπΉ) β β’ (π β NrmMod β Β· β ((πΎ Γt π½) Cn π½)) | ||
Theorem | rlmnlm 24204 | The ring module over a normed ring is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmRing β (ringLModβπ ) β NrmMod) | ||
Theorem | rlmnm 24205 | The norm function in the ring module. (Contributed by AV, 9-Oct-2021.) |
β’ (normβπ ) = (normβ(ringLModβπ )) | ||
Theorem | nrgtrg 24206 | A normed ring is a topological ring. (Contributed by Mario Carneiro, 4-Oct-2015.) (Proof shortened by AV, 31-Oct-2024.) |
β’ (π β NrmRing β π β TopRing) | ||
Theorem | nrginvrcnlem 24207* | Lemma for nrginvrcn 24208. Compare this proof with reccn2 15540, the elementary proof of continuity of division. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π = (Baseβπ ) & β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) & β’ π = (normβπ ) & β’ π· = (distβπ ) & β’ (π β π β NrmRing) & β’ (π β π β NzRing) & β’ (π β π΄ β π) & β’ (π β π΅ β β+) & β’ π = (if(1 β€ ((πβπ΄) Β· π΅), 1, ((πβπ΄) Β· π΅)) Β· ((πβπ΄) / 2)) β β’ (π β βπ₯ β β+ βπ¦ β π ((π΄π·π¦) < π₯ β ((πΌβπ΄)π·(πΌβπ¦)) < π΅)) | ||
Theorem | nrginvrcn 24208 | The ring inverse function is continuous in a normed ring. (Note that this is true even in rings which are not division rings.) (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π = (Baseβπ ) & β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) & β’ π½ = (TopOpenβπ ) β β’ (π β NrmRing β πΌ β ((π½ βΎt π) Cn (π½ βΎt π))) | ||
Theorem | nrgtdrg 24209 | A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ ((π β NrmRing β§ π β DivRing) β π β TopDRing) | ||
Theorem | nlmtlm 24210 | A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ (π β NrmMod β π β TopMod) | ||
Theorem | isnvc 24211 | A normed vector space is just a normed module which is algebraically a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmVec β (π β NrmMod β§ π β LVec)) | ||
Theorem | nvcnlm 24212 | A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmVec β π β NrmMod) | ||
Theorem | nvclvec 24213 | A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmVec β π β LVec) | ||
Theorem | nvclmod 24214 | A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmVec β π β LMod) | ||
Theorem | isnvc2 24215 | A normed vector space is just a normed module whose scalar ring is a division ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β NrmVec β (π β NrmMod β§ πΉ β DivRing)) | ||
Theorem | nvctvc 24216 | A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmVec β π β TopVec) | ||
Theorem | lssnlm 24217 | A subspace of a normed module is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) β β’ ((π β NrmMod β§ π β π) β π β NrmMod) | ||
Theorem | lssnvc 24218 | A subspace of a normed vector space is a normed vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) β β’ ((π β NrmVec β§ π β π) β π β NrmVec) | ||
Theorem | rlmnvc 24219 | The ring module over a normed division ring is a normed vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ ((π β NrmRing β§ π β DivRing) β (ringLModβπ ) β NrmVec) | ||
Theorem | ngpocelbl 24220 | Membership of an off-center vector in a ball in a normed module. (Contributed by NM, 27-Dec-2007.) (Revised by AV, 14-Oct-2021.) |
β’ π = (normβπΊ) & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π· = ((distβπΊ) βΎ (π Γ π)) β β’ ((πΊ β NrmMod β§ π β β* β§ (π β π β§ π΄ β π)) β ((π + π΄) β (π(ballβπ·)π ) β (πβπ΄) < π )) | ||
Syntax | cnmo 24221 | The operator norm function. |
class normOp | ||
Syntax | cnghm 24222 | The class of normed group homomorphisms. |
class NGHom | ||
Syntax | cnmhm 24223 | The class of normed module homomorphisms. |
class NMHom | ||
Definition | df-nmo 24224* | Define the norm of an operator between two normed groups (usually vector spaces). This definition produces an operator norm function for each pair of groups β¨π , π‘β©. Equivalent to the definition of linear operator norm in [AkhiezerGlazman] p. 39. (Contributed by Mario Carneiro, 18-Oct-2015.) (Revised by AV, 25-Sep-2020.) |
β’ normOp = (π β NrmGrp, π‘ β NrmGrp β¦ (π β (π GrpHom π‘) β¦ inf({π β (0[,)+β) β£ βπ₯ β (Baseβπ )((normβπ‘)β(πβπ₯)) β€ (π Β· ((normβπ )βπ₯))}, β*, < ))) | ||
Definition | df-nghm 24225* | Define the set of normed group homomorphisms between two normed groups. A normed group homomorphism is a group homomorphism which additionally bounds the increase of norm by a fixed real operator. In vector spaces these are also known as bounded linear operators. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ NGHom = (π β NrmGrp, π‘ β NrmGrp β¦ (β‘(π normOp π‘) β β)) | ||
Definition | df-nmhm 24226* | Define a normed module homomorphism, also known as a bounded linear operator. This is a module homomorphism (a linear function) such that the operator norm is finite, or equivalently there is a constant π such that... (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ NMHom = (π β NrmMod, π‘ β NrmMod β¦ ((π LMHom π‘) β© (π NGHom π‘))) | ||
Theorem | nmoffn 24227 | The function producing operator norm functions is a function on normed groups. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.) |
β’ normOp Fn (NrmGrp Γ NrmGrp) | ||
Theorem | reldmnghm 24228 | Lemma for normed group homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ Rel dom NGHom | ||
Theorem | reldmnmhm 24229 | Lemma for module homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ Rel dom NMHom | ||
Theorem | nmofval 24230* | Value of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Revised by AV, 26-Sep-2020.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΏ = (normβπ) & β’ π = (normβπ) β β’ ((π β NrmGrp β§ π β NrmGrp) β π = (π β (π GrpHom π) β¦ inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, < ))) | ||
Theorem | nmoval 24231* | Value of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Revised by AV, 26-Sep-2020.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΏ = (normβπ) & β’ π = (normβπ) β β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πβπΉ) = inf({π β (0[,)+β) β£ βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯))}, β*, < )) | ||
Theorem | nmogelb 24232* | Property of the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΏ = (normβπ) & β’ π = (normβπ) β β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π΄ β β*) β (π΄ β€ (πβπΉ) β βπ β (0[,)+β)(βπ₯ β π (πβ(πΉβπ₯)) β€ (π Β· (πΏβπ₯)) β π΄ β€ π))) | ||
Theorem | nmolb 24233* | Any upper bound on the values of a linear operator translates to an upper bound on the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΏ = (normβπ) & β’ π = (normβπ) β β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π΄ β β β§ 0 β€ π΄) β (βπ₯ β π (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯)) β (πβπΉ) β€ π΄)) | ||
Theorem | nmolb2d 24234* | Any upper bound on the values of a linear operator at nonzero vectors translates to an upper bound on the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΏ = (normβπ) & β’ π = (normβπ) & β’ 0 = (0gβπ) & β’ (π β π β NrmGrp) & β’ (π β π β NrmGrp) & β’ (π β πΉ β (π GrpHom π)) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ ((π β§ (π₯ β π β§ π₯ β 0 )) β (πβ(πΉβπ₯)) β€ (π΄ Β· (πΏβπ₯))) β β’ (π β (πβπΉ) β€ π΄) | ||
Theorem | nmof 24235 | The operator norm is a function into the extended reals. (Contributed by Mario Carneiro, 18-Oct-2015.) (Proof shortened by AV, 26-Sep-2020.) |
β’ π = (π normOp π) β β’ ((π β NrmGrp β§ π β NrmGrp) β π:(π GrpHom π)βΆβ*) | ||
Theorem | nmocl 24236 | The operator norm of an operator is an extended real. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) β β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πβπΉ) β β*) | ||
Theorem | nmoge0 24237 | The operator norm of an operator is nonnegative. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) β β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β 0 β€ (πβπΉ)) | ||
Theorem | nghmfval 24238 | A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) β β’ (π NGHom π) = (β‘π β β) | ||
Theorem | isnghm 24239 | A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) β β’ (πΉ β (π NGHom π) β ((π β NrmGrp β§ π β NrmGrp) β§ (πΉ β (π GrpHom π) β§ (πβπΉ) β β))) | ||
Theorem | isnghm2 24240 | A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) β β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πΉ β (π NGHom π) β (πβπΉ) β β)) | ||
Theorem | isnghm3 24241 | A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) β β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πΉ β (π NGHom π) β (πβπΉ) < +β)) | ||
Theorem | bddnghm 24242 | A bounded group homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) β β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π΄ β β β§ (πβπΉ) β€ π΄)) β πΉ β (π NGHom π)) | ||
Theorem | nghmcl 24243 | A normed group homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) β β’ (πΉ β (π NGHom π) β (πβπΉ) β β) | ||
Theorem | nmoi 24244 | The operator norm achieves the minimum of the set of upper bounds, if the operator is bounded. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΏ = (normβπ) & β’ π = (normβπ) β β’ ((πΉ β (π NGHom π) β§ π β π) β (πβ(πΉβπ)) β€ ((πβπΉ) Β· (πΏβπ))) | ||
Theorem | nmoix 24245 | The operator norm is a bound on the size of an operator, even when it is infinite (using extended real multiplication). (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΏ = (normβπ) & β’ π = (normβπ) β β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ π β π) β (πβ(πΉβπ)) β€ ((πβπΉ) Β·e (πΏβπ))) | ||
Theorem | nmoi2 24246 | The operator norm is a bound on the growth of a vector under the action of the operator. (Contributed by Mario Carneiro, 19-Oct-2015.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΏ = (normβπ) & β’ π = (normβπ) & β’ 0 = (0gβπ) β β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π β π β§ π β 0 )) β ((πβ(πΉβπ)) / (πΏβπ)) β€ (πβπΉ)) | ||
Theorem | nmoleub 24247* | The operator norm, defined as an infimum of upper bounds, can also be defined as a supremum of norms of πΉ(π₯) away from zero. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΏ = (normβπ) & β’ π = (normβπ) & β’ 0 = (0gβπ) & β’ (π β π β NrmGrp) & β’ (π β π β NrmGrp) & β’ (π β πΉ β (π GrpHom π)) & β’ (π β π΄ β β*) & β’ (π β 0 β€ π΄) β β’ (π β ((πβπΉ) β€ π΄ β βπ₯ β π (π₯ β 0 β ((πβ(πΉβπ₯)) / (πΏβπ₯)) β€ π΄))) | ||
Theorem | nghmrcl1 24248 | Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ (πΉ β (π NGHom π) β π β NrmGrp) | ||
Theorem | nghmrcl2 24249 | Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ (πΉ β (π NGHom π) β π β NrmGrp) | ||
Theorem | nghmghm 24250 | A normed group homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ (πΉ β (π NGHom π) β πΉ β (π GrpHom π)) | ||
Theorem | nmo0 24251 | The operator norm of the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) β β’ ((π β NrmGrp β§ π β NrmGrp) β (πβ(π Γ { 0 })) = 0) | ||
Theorem | nmoeq0 24252 | The operator norm is zero only for the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) β β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β ((πβπΉ) = 0 β πΉ = (π Γ { 0 }))) | ||
Theorem | nmoco 24253 | An upper bound on the operator norm of a composition. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π = (π normOp π) & β’ πΏ = (π normOp π) & β’ π = (π normOp π) β β’ ((πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β (πβ(πΉ β πΊ)) β€ ((πΏβπΉ) Β· (πβπΊ))) | ||
Theorem | nghmco 24254 | The composition of normed group homomorphisms is a normed group homomorphism. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ ((πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β (πΉ β πΊ) β (π NGHom π)) | ||
Theorem | nmotri 24255 | Triangle inequality for the operator norm. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π = (π normOp π) & β’ + = (+gβπ) β β’ ((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β (πβ(πΉ βf + πΊ)) β€ ((πβπΉ) + (πβπΊ))) | ||
Theorem | nghmplusg 24256 | The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ + = (+gβπ) β β’ ((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β (πΉ βf + πΊ) β (π NGHom π)) | ||
Theorem | 0nghm 24257 | The zero operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) β β’ ((π β NrmGrp β§ π β NrmGrp) β (π Γ { 0 }) β (π NGHom π)) | ||
Theorem | nmoid 24258 | The operator norm of the identity function on a nontrivial group. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) β β’ ((π β NrmGrp β§ { 0 } β π) β (πβ( I βΎ π)) = 1) | ||
Theorem | idnghm 24259 | The identity operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (Baseβπ) β β’ (π β NrmGrp β ( I βΎ π) β (π NGHom π)) | ||
Theorem | nmods 24260 | Upper bound for the distance between the values of a bounded linear operator. (Contributed by Mario Carneiro, 22-Oct-2015.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ πΆ = (distβπ) & β’ π· = (distβπ) β β’ ((πΉ β (π NGHom π) β§ π΄ β π β§ π΅ β π) β ((πΉβπ΄)π·(πΉβπ΅)) β€ ((πβπΉ) Β· (π΄πΆπ΅))) | ||
Theorem | nghmcn 24261 | A normed group homomorphism is a continuous function. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π½ = (TopOpenβπ) & β’ πΎ = (TopOpenβπ) β β’ (πΉ β (π NGHom π) β πΉ β (π½ Cn πΎ)) | ||
Theorem | isnmhm 24262 | A normed module homomorphism is a left module homomorphism which is also a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ (πΉ β (π NMHom π) β ((π β NrmMod β§ π β NrmMod) β§ (πΉ β (π LMHom π) β§ πΉ β (π NGHom π)))) | ||
Theorem | nmhmrcl1 24263 | Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ (πΉ β (π NMHom π) β π β NrmMod) | ||
Theorem | nmhmrcl2 24264 | Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ (πΉ β (π NMHom π) β π β NrmMod) | ||
Theorem | nmhmlmhm 24265 | A normed module homomorphism is a left module homomorphism (a linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ (πΉ β (π NMHom π) β πΉ β (π LMHom π)) | ||
Theorem | nmhmnghm 24266 | A normed module homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ (πΉ β (π NMHom π) β πΉ β (π NGHom π)) | ||
Theorem | nmhmghm 24267 | A normed module homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ (πΉ β (π NMHom π) β πΉ β (π GrpHom π)) | ||
Theorem | isnmhm2 24268 | A normed module homomorphism is a left module homomorphism with bounded norm (a bounded linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) β β’ ((π β NrmMod β§ π β NrmMod β§ πΉ β (π LMHom π)) β (πΉ β (π NMHom π) β (πβπΉ) β β)) | ||
Theorem | nmhmcl 24269 | A normed module homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) β β’ (πΉ β (π NMHom π) β (πβπΉ) β β) | ||
Theorem | idnmhm 24270 | The identity operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π = (Baseβπ) β β’ (π β NrmMod β ( I βΎ π) β (π NMHom π)) | ||
Theorem | 0nmhm 24271 | The zero operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (Scalarβπ) & β’ πΊ = (Scalarβπ) β β’ ((π β NrmMod β§ π β NrmMod β§ πΉ = πΊ) β (π Γ { 0 }) β (π NMHom π)) | ||
Theorem | nmhmco 24272 | The composition of bounded linear operators is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ ((πΉ β (π NMHom π) β§ πΊ β (π NMHom π)) β (πΉ β πΊ) β (π NMHom π)) | ||
Theorem | nmhmplusg 24273 | The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ + = (+gβπ) β β’ ((πΉ β (π NMHom π) β§ πΊ β (π NMHom π)) β (πΉ βf + πΊ) β (π NMHom π)) | ||
Theorem | qtopbaslem 24274 | The set of open intervals with endpoints in a subset forms a basis for a topology. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ π β β* β β’ ((,) β (π Γ π)) β TopBases | ||
Theorem | qtopbas 24275 | The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.) |
β’ ((,) β (β Γ β)) β TopBases | ||
Theorem | retopbas 24276 | 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 24277 | The standard topology on the reals. (Contributed by FL, 4-Jun-2007.) |
β’ (topGenβran (,)) β Top | ||
Theorem | uniretop 24278 | The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.) |
β’ β = βͺ (topGenβran (,)) | ||
Theorem | retopon 24279 | The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ (topGenβran (,)) β (TopOnββ) | ||
Theorem | retps 24280 | The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.) |
β’ πΎ = {β¨(Baseβndx), ββ©, β¨(TopSetβndx), (topGenβran (,))β©} β β’ πΎ β TopSp | ||
Theorem | iooretop 24281 | Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.) |
β’ (π΄(,)π΅) β (topGenβran (,)) | ||
Theorem | icccld 24282 | Closed intervals are closed sets of the standard topology on β. (Contributed by FL, 14-Sep-2007.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β (Clsdβ(topGenβran (,)))) | ||
Theorem | icopnfcld 24283 | Right-unbounded closed intervals are closed sets of the standard topology on β. (Contributed by Mario Carneiro, 17-Feb-2015.) |
β’ (π΄ β β β (π΄[,)+β) β (Clsdβ(topGenβran (,)))) | ||
Theorem | iocmnfcld 24284 | Left-unbounded closed intervals are closed sets of the standard topology on β. (Contributed by Mario Carneiro, 17-Feb-2015.) |
β’ (π΄ β β β (-β(,]π΄) β (Clsdβ(topGenβran (,)))) | ||
Theorem | qdensere 24285 | β is dense in the standard topology on β. (Contributed by NM, 1-Mar-2007.) |
β’ ((clsβ(topGenβran (,)))ββ) = β | ||
Theorem | cnmetdval 24286 | 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 24287 | 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 24288 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ (abs β β ) β (βMetββ) | ||
Theorem | cnbl0 24289 | Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
β’ π· = (abs β β ) β β’ (π β β* β (β‘abs β (0[,)π )) = (0(ballβπ·)π )) | ||
Theorem | cnblcld 24290* | Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
β’ π· = (abs β β ) β β’ (π β β* β (β‘abs β (0[,]π )) = {π₯ β β β£ (0π·π₯) β€ π }) | ||
Theorem | cnfldms 24291 | The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ βfld β MetSp | ||
Theorem | cnfldxms 24292 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ βfld β βMetSp | ||
Theorem | cnfldtps 24293 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ βfld β TopSp | ||
Theorem | cnfldnm 24294 | The norm of the field of complex numbers. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ abs = (normββfld) | ||
Theorem | cnngp 24295 | The complex numbers form a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ βfld β NrmGrp | ||
Theorem | cnnrg 24296 | The complex numbers form a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ βfld β NrmRing | ||
Theorem | cnfldtopn 24297 | The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π½ = (TopOpenββfld) β β’ π½ = (MetOpenβ(abs β β )) | ||
Theorem | cnfldtopon 24298 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π½ = (TopOpenββfld) β β’ π½ β (TopOnββ) | ||
Theorem | cnfldtop 24299 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π½ = (TopOpenββfld) β β’ π½ β Top | ||
Theorem | cnfldhaus 24300 | The topology of the complex numbers is Hausdorff. (Contributed by Mario Carneiro, 8-Sep-2015.) |
β’ π½ = (TopOpenββfld) β β’ π½ β Haus |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |