![]() |
Metamath
Proof Explorer Theorem List (p. 245 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nmmul 24401 | The norm of a product in a normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (Baseβπ ) & β’ π = (normβπ ) & β’ Β· = (.rβπ ) β β’ ((π β NrmRing β§ π΄ β π β§ π΅ β π) β (πβ(π΄ Β· π΅)) = ((πβπ΄) Β· (πβπ΅))) | ||
Theorem | nrgdsdi 24402 | Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (Baseβπ ) & β’ π = (normβπ ) & β’ Β· = (.rβπ ) & β’ π· = (distβπ ) β β’ ((π β NrmRing β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((πβπ΄) Β· (π΅π·πΆ)) = ((π΄ Β· π΅)π·(π΄ Β· πΆ))) | ||
Theorem | nrgdsdir 24403 | Distribute a distance calculation. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (Baseβπ ) & β’ π = (normβπ ) & β’ Β· = (.rβπ ) & β’ π· = (distβπ ) β β’ ((π β NrmRing β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅) Β· (πβπΆ)) = ((π΄ Β· πΆ)π·(π΅ Β· πΆ))) | ||
Theorem | nm1 24404 | The norm of one in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (normβπ ) & β’ 1 = (1rβπ ) β β’ ((π β NrmRing β§ π β NzRing) β (πβ 1 ) = 1) | ||
Theorem | unitnmn0 24405 | The norm of a unit is nonzero in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (normβπ ) & β’ π = (Unitβπ ) β β’ ((π β NrmRing β§ π β NzRing β§ π΄ β π) β (πβπ΄) β 0) | ||
Theorem | nminvr 24406 | The norm of an inverse in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (normβπ ) & β’ π = (Unitβπ ) & β’ πΌ = (invrβπ ) β β’ ((π β NrmRing β§ π β NzRing β§ π΄ β π) β (πβ(πΌβπ΄)) = (1 / (πβπ΄))) | ||
Theorem | nmdvr 24407 | The norm of a division in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ π = (Baseβπ ) & β’ π = (normβπ ) & β’ π = (Unitβπ ) & β’ / = (/rβπ ) β β’ (((π β NrmRing β§ π β NzRing) β§ (π΄ β π β§ π΅ β π)) β (πβ(π΄ / π΅)) = ((πβπ΄) / (πβπ΅))) | ||
Theorem | nrgdomn 24408 | A nonzero normed ring is a domain. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmRing β (π β Domn β π β NzRing)) | ||
Theorem | nrgtgp 24409 | A normed ring is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (π β NrmRing β π β TopGrp) | ||
Theorem | subrgnrg 24410 | A normed ring restricted to a subring is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π» = (πΊ βΎs π΄) β β’ ((πΊ β NrmRing β§ π΄ β (SubRingβπΊ)) β π» β NrmRing) | ||
Theorem | tngnrg 24411 | Given any absolute value over a ring, augmenting the ring with the absolute value produces a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (π toNrmGrp πΉ) & β’ π΄ = (AbsValβπ ) β β’ (πΉ β π΄ β π β NrmRing) | ||
Theorem | isnlm 24412* | A normed (left) module is a module which is also a normed group over a normed ring, such that the norm distributes over scalar multiplication. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π΄ = (normβπΉ) β β’ (π β NrmMod β ((π β NrmGrp β§ π β LMod β§ πΉ β NrmRing) β§ βπ₯ β πΎ βπ¦ β π (πβ(π₯ Β· π¦)) = ((π΄βπ₯) Β· (πβπ¦)))) | ||
Theorem | nmvs 24413 | Defining property of a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π΄ = (normβπΉ) β β’ ((π β NrmMod β§ π β πΎ β§ π β π) β (πβ(π Β· π)) = ((π΄βπ) Β· (πβπ))) | ||
Theorem | nlmngp 24414 | A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmMod β π β NrmGrp) | ||
Theorem | nlmlmod 24415 | A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmMod β π β LMod) | ||
Theorem | nlmnrg 24416 | The scalar component of a left module is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β NrmMod β πΉ β NrmRing) | ||
Theorem | nlmngp2 24417 | The scalar component of a left module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β NrmMod β πΉ β NrmGrp) | ||
Theorem | nlmdsdi 24418 | Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π· = (distβπ) & β’ π΄ = (normβπΉ) β β’ ((π β NrmMod β§ (π β πΎ β§ π β π β§ π β π)) β ((π΄βπ) Β· (ππ·π)) = ((π Β· π)π·(π Β· π))) | ||
Theorem | nlmdsdir 24419 | Distribute a distance calculation. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π· = (distβπ) & β’ π = (normβπ) & β’ πΈ = (distβπΉ) β β’ ((π β NrmMod β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((ππΈπ) Β· (πβπ)) = ((π Β· π)π·(π Β· π))) | ||
Theorem | nlmmul0or 24420 | If a scalar product is zero, one of its factors must be zero. (Contributed by NM, 6-Dec-2007.) (Revised by Mario Carneiro, 4-Oct-2015.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (0gβπΉ) β β’ ((π β NrmMod β§ π΄ β πΎ β§ π΅ β π) β ((π΄ Β· π΅) = 0 β (π΄ = π β¨ π΅ = 0 ))) | ||
Theorem | sranlm 24421 | The subring algebra over a normed ring is a normed left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π΄ = ((subringAlg βπ)βπ) β β’ ((π β NrmRing β§ π β (SubRingβπ)) β π΄ β NrmMod) | ||
Theorem | nlmvscnlem2 24422 | Lemma for nlmvscn 24424. Compare this proof with the similar elementary proof mulcn2 15544 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 24423* | Lemma for nlmvscn 24424. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ π = (Baseβπ) & β’ πΎ = (BaseβπΉ) & β’ π· = (distβπ) & β’ πΈ = (distβπΉ) & β’ π = (normβπ) & β’ π΄ = (normβπΉ) & β’ Β· = ( Β·π βπ) & β’ π = ((π / 2) / ((π΄βπ΅) + 1)) & β’ π = ((π / 2) / ((πβπ) + π)) & β’ (π β π β NrmMod) & β’ (π β π β β+) & β’ (π β π΅ β πΎ) & β’ (π β π β π) β β’ (π β βπ β β+ βπ₯ β πΎ βπ¦ β π (((π΅πΈπ₯) < π β§ (ππ·π¦) < π) β ((π΅ Β· π)π·(π₯ Β· π¦)) < π )) | ||
Theorem | nlmvscn 24424 | The scalar multiplication of a normed module is continuous. Lemma for nrgtrg 24427 and nlmtlm 24431. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·sf βπ) & β’ π½ = (TopOpenβπ) & β’ πΎ = (TopOpenβπΉ) β β’ (π β NrmMod β Β· β ((πΎ Γt π½) Cn π½)) | ||
Theorem | rlmnlm 24425 | The ring module over a normed ring is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmRing β (ringLModβπ ) β NrmMod) | ||
Theorem | rlmnm 24426 | The norm function in the ring module. (Contributed by AV, 9-Oct-2021.) |
β’ (normβπ ) = (normβ(ringLModβπ )) | ||
Theorem | nrgtrg 24427 | 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 24428* | Lemma for nrginvrcn 24429. Compare this proof with reccn2 15545, 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 24429 | 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 24430 | A normed division ring is a topological division ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ ((π β NrmRing β§ π β DivRing) β π β TopDRing) | ||
Theorem | nlmtlm 24431 | A normed module is a topological module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ (π β NrmMod β π β TopMod) | ||
Theorem | isnvc 24432 | 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 24433 | A normed vector space is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmVec β π β NrmMod) | ||
Theorem | nvclvec 24434 | A normed vector space is a left vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmVec β π β LVec) | ||
Theorem | nvclmod 24435 | A normed vector space is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmVec β π β LMod) | ||
Theorem | isnvc2 24436 | 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 24437 | A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmVec β π β TopVec) | ||
Theorem | lssnlm 24438 | A subspace of a normed module is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) β β’ ((π β NrmMod β§ π β π) β π β NrmMod) | ||
Theorem | lssnvc 24439 | 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 24440 | 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 24441 | 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 24442 | The operator norm function. |
class normOp | ||
Syntax | cnghm 24443 | The class of normed group homomorphisms. |
class NGHom | ||
Syntax | cnmhm 24444 | The class of normed module homomorphisms. |
class NMHom | ||
Definition | df-nmo 24445* | 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 24446* | 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 24447* | 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 24448 | 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 24449 | Lemma for normed group homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ Rel dom NGHom | ||
Theorem | reldmnmhm 24450 | Lemma for module homomorphisms. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ Rel dom NMHom | ||
Theorem | nmofval 24451* | 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 24452* | 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 24453* | 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 24454* | 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 24455* | 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 24456 | 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 24457 | The operator norm of an operator is an extended real. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) β β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β (πβπΉ) β β*) | ||
Theorem | nmoge0 24458 | The operator norm of an operator is nonnegative. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) β β’ ((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β 0 β€ (πβπΉ)) | ||
Theorem | nghmfval 24459 | A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) β β’ (π NGHom π) = (β‘π β β) | ||
Theorem | isnghm 24460 | 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 24461 | 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 24462 | 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 24463 | A bounded group homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) β β’ (((π β NrmGrp β§ π β NrmGrp β§ πΉ β (π GrpHom π)) β§ (π΄ β β β§ (πβπΉ) β€ π΄)) β πΉ β (π NGHom π)) | ||
Theorem | nghmcl 24464 | A normed group homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) β β’ (πΉ β (π NGHom π) β (πβπΉ) β β) | ||
Theorem | nmoi 24465 | 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 24466 | 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 24467 | 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 24468* | 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 24469 | Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ (πΉ β (π NGHom π) β π β NrmGrp) | ||
Theorem | nghmrcl2 24470 | Reverse closure for a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ (πΉ β (π NGHom π) β π β NrmGrp) | ||
Theorem | nghmghm 24471 | A normed group homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ (πΉ β (π NGHom π) β πΉ β (π GrpHom π)) | ||
Theorem | nmo0 24472 | The operator norm of the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π = (π normOp π) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) β β’ ((π β NrmGrp β§ π β NrmGrp) β (πβ(π Γ { 0 })) = 0) | ||
Theorem | nmoeq0 24473 | 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 24474 | An upper bound on the operator norm of a composition. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π = (π normOp π) & β’ πΏ = (π normOp π) & β’ π = (π normOp π) β β’ ((πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β (πβ(πΉ β πΊ)) β€ ((πΏβπΉ) Β· (πβπΊ))) | ||
Theorem | nghmco 24475 | The composition of normed group homomorphisms is a normed group homomorphism. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ ((πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β (πΉ β πΊ) β (π NGHom π)) | ||
Theorem | nmotri 24476 | Triangle inequality for the operator norm. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π = (π normOp π) & β’ + = (+gβπ) β β’ ((π β Abel β§ πΉ β (π NGHom π) β§ πΊ β (π NGHom π)) β (πβ(πΉ βf + πΊ)) β€ ((πβπΉ) + (πβπΊ))) | ||
Theorem | nghmplusg 24477 | 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 24478 | The zero operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) β β’ ((π β NrmGrp β§ π β NrmGrp) β (π Γ { 0 }) β (π NGHom π)) | ||
Theorem | nmoid 24479 | 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 24480 | The identity operator is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (Baseβπ) β β’ (π β NrmGrp β ( I βΎ π) β (π NGHom π)) | ||
Theorem | nmods 24481 | 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 24482 | A normed group homomorphism is a continuous function. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π½ = (TopOpenβπ) & β’ πΎ = (TopOpenβπ) β β’ (πΉ β (π NGHom π) β πΉ β (π½ Cn πΎ)) | ||
Theorem | isnmhm 24483 | 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 24484 | Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ (πΉ β (π NMHom π) β π β NrmMod) | ||
Theorem | nmhmrcl2 24485 | Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ (πΉ β (π NMHom π) β π β NrmMod) | ||
Theorem | nmhmlmhm 24486 | A normed module homomorphism is a left module homomorphism (a linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ (πΉ β (π NMHom π) β πΉ β (π LMHom π)) | ||
Theorem | nmhmnghm 24487 | A normed module homomorphism is a normed group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ (πΉ β (π NMHom π) β πΉ β (π NGHom π)) | ||
Theorem | nmhmghm 24488 | A normed module homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ (πΉ β (π NMHom π) β πΉ β (π GrpHom π)) | ||
Theorem | isnmhm2 24489 | 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 24490 | A normed module homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
β’ π = (π normOp π) β β’ (πΉ β (π NMHom π) β (πβπΉ) β β) | ||
Theorem | idnmhm 24491 | The identity operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π = (Baseβπ) β β’ (π β NrmMod β ( I βΎ π) β (π NMHom π)) | ||
Theorem | 0nmhm 24492 | 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 24493 | The composition of bounded linear operators is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ ((πΉ β (π NMHom π) β§ πΊ β (π NMHom π)) β (πΉ β πΊ) β (π NMHom π)) | ||
Theorem | nmhmplusg 24494 | The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ + = (+gβπ) β β’ ((πΉ β (π NMHom π) β§ πΊ β (π NMHom π)) β (πΉ βf + πΊ) β (π NMHom π)) | ||
Theorem | qtopbaslem 24495 | 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 24496 | The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.) |
β’ ((,) β (β Γ β)) β TopBases | ||
Theorem | retopbas 24497 | 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 24498 | The standard topology on the reals. (Contributed by FL, 4-Jun-2007.) |
β’ (topGenβran (,)) β Top | ||
Theorem | uniretop 24499 | The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.) |
β’ β = βͺ (topGenβran (,)) | ||
Theorem | retopon 24500 | The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ (topGenβran (,)) β (TopOnββ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |