![]() |
Metamath
Proof Explorer Theorem List (p. 244 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | metucn 24301* | Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn 24273. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ π = (metUnifβπΆ) & β’ π = (metUnifβπ·) & β’ (π β π β β ) & β’ (π β π β β ) & β’ (π β πΆ β (PsMetβπ)) & β’ (π β π· β (PsMetβπ)) β β’ (π β (πΉ β (π Cnuπ) β (πΉ:πβΆπ β§ βπ β β+ βπ β β+ βπ₯ β π βπ¦ β π ((π₯πΆπ¦) < π β ((πΉβπ₯)π·(πΉβπ¦)) < π)))) | ||
Theorem | dscmet 24302* | The discrete metric on any set π. Definition 1.1-8 of [Kreyszig] p. 8. (Contributed by FL, 12-Oct-2006.) |
β’ π· = (π₯ β π, π¦ β π β¦ if(π₯ = π¦, 0, 1)) β β’ (π β π β π· β (Metβπ)) | ||
Theorem | dscopn 24303* | The discrete metric generates the discrete topology. In particular, the discrete topology is metrizable. (Contributed by Mario Carneiro, 29-Jan-2014.) |
β’ π· = (π₯ β π, π¦ β π β¦ if(π₯ = π¦, 0, 1)) β β’ (π β π β (MetOpenβπ·) = π« π) | ||
Theorem | nrmmetd 24304* | Show that a group norm generates a metric. Part of Definition 2.2-1 of [Kreyszig] p. 58. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β Grp) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π₯ β π) β ((πΉβπ₯) = 0 β π₯ = 0 )) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πΉβ(π₯ β π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) β β’ (π β (πΉ β β ) β (Metβπ)) | ||
Theorem | abvmet 24305 | An absolute value πΉ generates a metric defined by π(π₯, π¦) = πΉ(π₯ β π¦), analogously to cnmet 24509. (In fact, the ring structure is not needed at all; the group properties abveq0 20578 and abvtri 20582, abvneg 20586 are sufficient.) (Contributed by Mario Carneiro, 9-Sep-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (Baseβπ ) & β’ π΄ = (AbsValβπ ) & β’ β = (-gβπ ) β β’ (πΉ β π΄ β (πΉ β β ) β (Metβπ)) | ||
In the following, the norm of a normed algebraic structure (group, left module, vector space) is defined by the (given) distance function (the norm π of an element is its distance π· from the zero element, see nmval 24319: (πβπ΄) = (π΄π· 0 )). By this definition, the norm function π is actually a norm (satisfying the properties: being a function into the reals; subadditivity/triangle inequality (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦)); absolute homogeneity ( n(sx) = |s| n(x) ) [Remark: for group norms, some authors (e.g., Juris Steprans in "A characterization of free abelian groups") demand that n(sx) = |s| n(x) for all π β β€, whereas other authors (e.g., N. H. Bingham and A. J. Ostaszewski in "Normed versus topological groups: Dichotomy and duality") only require inversion symmetry, i.e., (πβ( β π₯) = πβπ₯). The definition df-ngp 24313 of a group norm follows the second aproach, see nminv 24351.] and positive definiteness/point-separation ((πβπ₯) = 0 β π₯ = 0)) if the structure is a metric space with a right-translation-invariant metric (see nmf 24345, nmtri 24356, nmvs 24414 and nmeq0 24348). An alternate definition of a normed group (i.e., a group equipped with a norm) not using the properties of a metric space is given by Theorem tngngp3 24394. The norm can be expressed as the distance to zero (nmfval 24318), so in a structure with a zero (a "pointed set", for instance a monoid or a group), the norm can be expressed as the distance restricted to the elements of the base set to zero (nmfval0 24320). Usually, however, the norm of a normed structure is given, and the corresponding metric ("induced metric") is defined as the distance function based on the norm (the distance π· between two elements is the norm π of their difference, see ngpds 24334: (π΄π·π΅) = (πβ(π΄ β π΅))). The operation toNrmGrp does exactly this, i.e., it adds a distance function (and a topology) to a structure (which should be at least a group for the difference of two elements to make sense) corresponding to a given norm as explained above: (distβπ) = (π β β ), see also tngds 24385. By this, the enhanced structure becomes a normed structure if the induced metric is in fact a metric (see tngngp2 24390) or a norm (see tngngpd 24391). If the norm is derived from a given metric, as done with df-nm 24312, the induced metric is the original metric restricted to the base set: (distβπ) = ((distβπΊ) βΎ (π Γ π)), see nrmtngdist 24395, and the norm remains the same: (normβπ) = (normβπΊ), see nrmtngnrm 24396. | ||
Syntax | cnm 24306 | Norm of a normed ring. |
class norm | ||
Syntax | cngp 24307 | The class of all normed groups. |
class NrmGrp | ||
Syntax | ctng 24308 | Make a normed group from a norm and a group. |
class toNrmGrp | ||
Syntax | cnrg 24309 | Normed ring. |
class NrmRing | ||
Syntax | cnlm 24310 | Normed module. |
class NrmMod | ||
Syntax | cnvc 24311 | Normed vector space. |
class NrmVec | ||
Definition | df-nm 24312* | Define the norm on a group or ring (when it makes sense) in terms of the distance to zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ norm = (π€ β V β¦ (π₯ β (Baseβπ€) β¦ (π₯(distβπ€)(0gβπ€)))) | ||
Definition | df-ngp 24313 | Define a normed group, which is a group with a right-translation-invariant metric. This is not a standard notion, but is helpful as the most general context in which a metric-like norm makes sense. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ NrmGrp = {π β (Grp β© MetSp) β£ ((normβπ) β (-gβπ)) β (distβπ)} | ||
Definition | df-tng 24314* | Define a function that fills in the topology and metric components of a structure given a group and a norm on it. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ toNrmGrp = (π β V, π β V β¦ ((π sSet β¨(distβndx), (π β (-gβπ))β©) sSet β¨(TopSetβndx), (MetOpenβ(π β (-gβπ)))β©)) | ||
Definition | df-nrg 24315 | A normed ring is a ring with an induced topology and metric such that the metric is translation-invariant and the norm (distance from 0) is an absolute value on the ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ NrmRing = {π€ β NrmGrp β£ (normβπ€) β (AbsValβπ€)} | ||
Definition | df-nlm 24316* | 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.) |
β’ NrmMod = {π€ β (NrmGrp β© LMod) β£ [(Scalarβπ€) / π](π β NrmRing β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ€)((normβπ€)β(π₯( Β·π βπ€)π¦)) = (((normβπ)βπ₯) Β· ((normβπ€)βπ¦)))} | ||
Definition | df-nvc 24317 | A normed vector space is a normed module which is also a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ NrmVec = (NrmMod β© LVec) | ||
Theorem | nmfval 24318* | The value of the norm function as the distance to zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = (distβπ) β β’ π = (π₯ β π β¦ (π₯π· 0 )) | ||
Theorem | nmval 24319 | The value of the norm as the distance to zero. Problem 1 of [Kreyszig] p. 63. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = (distβπ) β β’ (π΄ β π β (πβπ΄) = (π΄π· 0 )) | ||
Theorem | nmfval0 24320* | The value of the norm function on a structure containing a zero as the distance restricted to the elements of the base set to zero. Examples of structures containing a "zero" are groups (see nmfval2 24321 proved from this theorem and grpidcl 18887) or more generally monoids (see mndidcl 18675), or pointed sets). (Contributed by Mario Carneiro, 2-Oct-2015.) Extract this result from the proof of nmfval2 24321. (Revised by BJ, 27-Aug-2024.) |
β’ π = (normβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = (distβπ) & β’ πΈ = (π· βΎ (π Γ π)) β β’ ( 0 β π β π = (π₯ β π β¦ (π₯πΈ 0 ))) | ||
Theorem | nmfval2 24321* | The value of the norm function on a group as the distance restricted to the elements of the base set to zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = (distβπ) & β’ πΈ = (π· βΎ (π Γ π)) β β’ (π β Grp β π = (π₯ β π β¦ (π₯πΈ 0 ))) | ||
Theorem | nmval2 24322 | The value of the norm on a group as the distance restricted to the elements of the base set to zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = (distβπ) & β’ πΈ = (π· βΎ (π Γ π)) β β’ ((π β Grp β§ π΄ β π) β (πβπ΄) = (π΄πΈ 0 )) | ||
Theorem | nmf2 24323 | The norm on a metric group is a function from the base set into the reals. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπ) & β’ π = (Baseβπ) & β’ π· = (distβπ) & β’ πΈ = (π· βΎ (π Γ π)) β β’ ((π β Grp β§ πΈ β (Metβπ)) β π:πβΆβ) | ||
Theorem | nmpropd 24324 | Weak property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β (BaseβπΎ) = (BaseβπΏ)) & β’ (π β (+gβπΎ) = (+gβπΏ)) & β’ (π β (distβπΎ) = (distβπΏ)) β β’ (π β (normβπΎ) = (normβπΏ)) | ||
Theorem | nmpropd2 24325* | Strong property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β πΎ β Grp) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ (π β ((distβπΎ) βΎ (π΅ Γ π΅)) = ((distβπΏ) βΎ (π΅ Γ π΅))) β β’ (π β (normβπΎ) = (normβπΏ)) | ||
Theorem | isngp 24326 | The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) β β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§ (π β β ) β π·)) | ||
Theorem | isngp2 24327 | The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) & β’ π = (BaseβπΊ) & β’ πΈ = (π· βΎ (π Γ π)) β β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§ (π β β ) = πΈ)) | ||
Theorem | isngp3 24328* | The property of being a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (normβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) & β’ π = (BaseβπΊ) β β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§ βπ₯ β π βπ¦ β π (π₯π·π¦) = (πβ(π₯ β π¦)))) | ||
Theorem | ngpgrp 24329 | A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ (πΊ β NrmGrp β πΊ β Grp) | ||
Theorem | ngpms 24330 | A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ (πΊ β NrmGrp β πΊ β MetSp) | ||
Theorem | ngpxms 24331 | A normed group is an extended metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ (πΊ β NrmGrp β πΊ β βMetSp) | ||
Theorem | ngptps 24332 | A normed group is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (πΊ β NrmGrp β πΊ β TopSp) | ||
Theorem | ngpmet 24333 | The (induced) metric of a normed group is a metric. Part of Definition 2.2-1 of [Kreyszig] p. 58. (Contributed by NM, 4-Dec-2006.) (Revised by AV, 14-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ π· = ((distβπΊ) βΎ (π Γ π)) β β’ (πΊ β NrmGrp β π· β (Metβπ)) | ||
Theorem | ngpds 24334 | Value of the distance function in terms of the norm of a normed group. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 28-Nov-2006.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπΊ) & β’ π = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (πβ(π΄ β π΅))) | ||
Theorem | ngpdsr 24335 | Value of the distance function in terms of the norm of a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπΊ) & β’ π = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (πβ(π΅ β π΄))) | ||
Theorem | ngpds2 24336 | Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = ((π΄ β π΅)π· 0 )) | ||
Theorem | ngpds2r 24337 | Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = ((π΅ β π΄)π· 0 )) | ||
Theorem | ngpds3 24338 | Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = ( 0 π·(π΄ β π΅))) | ||
Theorem | ngpds3r 24339 | Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = ( 0 π·(π΅ β π΄))) | ||
Theorem | ngprcan 24340 | Cancel right addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π· = (distβπΊ) β β’ ((πΊ β NrmGrp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ + πΆ)π·(π΅ + πΆ)) = (π΄π·π΅)) | ||
Theorem | ngplcan 24341 | Cancel left addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π· = (distβπΊ) β β’ (((πΊ β NrmGrp β§ πΊ β Abel) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((πΆ + π΄)π·(πΆ + π΅)) = (π΄π·π΅)) | ||
Theorem | isngp4 24342* | Express the property of being a normed group purely in terms of right-translation invariance of the metric instead of using the definition of norm (which itself uses the metric). (Contributed by Mario Carneiro, 29-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π· = (distβπΊ) β β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§ βπ₯ β π βπ¦ β π βπ§ β π ((π₯ + π§)π·(π¦ + π§)) = (π₯π·π¦))) | ||
Theorem | ngpinvds 24343 | Two elements are the same distance apart as their inverses. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ πΌ = (invgβπΊ) & β’ π· = (distβπΊ) β β’ (((πΊ β NrmGrp β§ πΊ β Abel) β§ (π΄ β π β§ π΅ β π)) β ((πΌβπ΄)π·(πΌβπ΅)) = (π΄π·π΅)) | ||
Theorem | ngpsubcan 24344 | Cancel right subtraction inside a distance calculation. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) β β’ ((πΊ β NrmGrp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ β πΆ)π·(π΅ β πΆ)) = (π΄π·π΅)) | ||
Theorem | nmf 24345 | The norm on a normed group is a function into the reals. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) β β’ (πΊ β NrmGrp β π:πβΆβ) | ||
Theorem | nmcl 24346 | The norm of a normed group is closed in the reals. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π) β (πβπ΄) β β) | ||
Theorem | nmge0 24347 | The norm of a normed group is nonnegative. Second part of Problem 2 of [Kreyszig] p. 64. (Contributed by NM, 28-Nov-2006.) (Revised by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π) β 0 β€ (πβπ΄)) | ||
Theorem | nmeq0 24348 | The identity is the only element of the group with zero norm. First part of Problem 2 of [Kreyszig] p. 64. (Contributed by NM, 24-Nov-2006.) (Revised by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π) β ((πβπ΄) = 0 β π΄ = 0 )) | ||
Theorem | nmne0 24349 | The norm of a nonzero element is nonzero. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΄ β 0 ) β (πβπ΄) β 0) | ||
Theorem | nmrpcl 24350 | The norm of a nonzero element is a positive real. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΄ β 0 ) β (πβπ΄) β β+) | ||
Theorem | nminv 24351 | The norm of a negated element is the same as the norm of the original element. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ πΌ = (invgβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π) β (πβ(πΌβπ΄)) = (πβπ΄)) | ||
Theorem | nmmtri 24352 | The triangle inequality for the norm of a subtraction. (Contributed by NM, 27-Dec-2007.) (Revised by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (πβ(π΄ β π΅)) β€ ((πβπ΄) + (πβπ΅))) | ||
Theorem | nmsub 24353 | The norm of the difference between two elements. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (πβ(π΄ β π΅)) = (πβ(π΅ β π΄))) | ||
Theorem | nmrtri 24354 | Reverse triangle inequality for the norm of a subtraction. Problem 3 of [Kreyszig] p. 64. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (absβ((πβπ΄) β (πβπ΅))) β€ (πβ(π΄ β π΅))) | ||
Theorem | nm2dif 24355 | Inequality for the difference of norms. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β ((πβπ΄) β (πβπ΅)) β€ (πβ(π΄ β π΅))) | ||
Theorem | nmtri 24356 | The triangle inequality for the norm of a sum. (Contributed by NM, 11-Nov-2006.) (Revised by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (πβ(π΄ + π΅)) β€ ((πβπ΄) + (πβπ΅))) | ||
Theorem | nmtri2 24357 | Triangle inequality for the norm of two subtractions. (Contributed by NM, 24-Feb-2008.) (Revised by AV, 8-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β NrmGrp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (πβ(π΄ β πΆ)) β€ ((πβ(π΄ β π΅)) + (πβ(π΅ β πΆ)))) | ||
Theorem | ngpi 24358* | The properties of a normed group, which is a group accompanied by a norm. (Contributed by AV, 7-Oct-2021.) |
β’ π = (Baseβπ) & β’ π = (normβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) β β’ (π β NrmGrp β (π β Grp β§ π:πβΆβ β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))))) | ||
Theorem | nm0 24359 | Norm of the identity element. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (normβπΊ) & β’ 0 = (0gβπΊ) β β’ (πΊ β NrmGrp β (πβ 0 ) = 0) | ||
Theorem | nmgt0 24360 | The norm of a nonzero element is a positive real. (Contributed by NM, 20-Nov-2007.) (Revised by AV, 8-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π) β (π΄ β 0 β 0 < (πβπ΄))) | ||
Theorem | sgrim 24361 | The induced metric on a subgroup is the induced metric on the parent group equipped with a norm. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 19-Oct-2021.) |
β’ π = (π βΎs π) & β’ π· = (distβπ) & β’ πΈ = (distβπ) β β’ (π β π β πΈ = π·) | ||
Theorem | sgrimval 24362 | The induced metric on a subgroup in terms of the induced metric on the parent normed group. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 19-Oct-2021.) |
β’ π = (π βΎs π) & β’ π· = (distβπ) & β’ πΈ = (distβπ) & β’ π = (πΊ toNrmGrp π) & β’ π = (normβπΊ) & β’ π = (SubGrpβπ) β β’ (((πΊ β NrmGrp β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π΄πΈπ΅) = (π΄π·π΅)) | ||
Theorem | subgnm 24363 | The norm in a subgroup. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π» = (πΊ βΎs π΄) & β’ π = (normβπΊ) & β’ π = (normβπ») β β’ (π΄ β (SubGrpβπΊ) β π = (π βΎ π΄)) | ||
Theorem | subgnm2 24364 | A substructure assigns the same values to the norms of elements of a subgroup. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π» = (πΊ βΎs π΄) & β’ π = (normβπΊ) & β’ π = (normβπ») β β’ ((π΄ β (SubGrpβπΊ) β§ π β π΄) β (πβπ) = (πβπ)) | ||
Theorem | subgngp 24365 | A normed group restricted to a subgroup is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π» = (πΊ βΎs π΄) β β’ ((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β π» β NrmGrp) | ||
Theorem | ngptgp 24366 | A normed abelian group is a topological group (with the topology induced by the metric induced by the norm). (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ ((πΊ β NrmGrp β§ πΊ β Abel) β πΊ β TopGrp) | ||
Theorem | ngppropd 24367* | Property deduction for a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ (π β ((distβπΎ) βΎ (π΅ Γ π΅)) = ((distβπΏ) βΎ (π΅ Γ π΅))) & β’ (π β (TopOpenβπΎ) = (TopOpenβπΏ)) β β’ (π β (πΎ β NrmGrp β πΏ β NrmGrp)) | ||
Theorem | reldmtng 24368 | The function toNrmGrp is a two-argument function. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ Rel dom toNrmGrp | ||
Theorem | tngval 24369 | Value of the function which augments a given structure πΊ with a norm π. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (πΊ toNrmGrp π) & β’ β = (-gβπΊ) & β’ π· = (π β β ) & β’ π½ = (MetOpenβπ·) β β’ ((πΊ β π β§ π β π) β π = ((πΊ sSet β¨(distβndx), π·β©) sSet β¨(TopSetβndx), π½β©)) | ||
Theorem | tnglem 24370 | Lemma for tngbas 24372 and similar theorems. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ πΈ = Slot (πΈβndx) & β’ (πΈβndx) β (TopSetβndx) & β’ (πΈβndx) β (distβndx) β β’ (π β π β (πΈβπΊ) = (πΈβπ)) | ||
Theorem | tnglemOLD 24371 | Obsolete version of tnglem 24370 as of 31-Oct-2024. Lemma for tngbas 24372 and similar theorems. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (πΊ toNrmGrp π) & β’ πΈ = Slot πΎ & β’ πΎ β β & β’ πΎ < 9 β β’ (π β π β (πΈβπΊ) = (πΈβπ)) | ||
Theorem | tngbas 24372 | The base set of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ π΅ = (BaseβπΊ) β β’ (π β π β π΅ = (Baseβπ)) | ||
Theorem | tngbasOLD 24373 | Obsolete proof of tngbas 24372 as of 31-Oct-2024. The base set of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (πΊ toNrmGrp π) & β’ π΅ = (BaseβπΊ) β β’ (π β π β π΅ = (Baseβπ)) | ||
Theorem | tngplusg 24374 | The group addition of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ + = (+gβπΊ) β β’ (π β π β + = (+gβπ)) | ||
Theorem | tngplusgOLD 24375 | Obsolete proof of tngplusg 24374 as of 31-Oct-2024. The group addition of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (πΊ toNrmGrp π) & β’ + = (+gβπΊ) β β’ (π β π β + = (+gβπ)) | ||
Theorem | tng0 24376 | The group identity of a structure augmented with a norm. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ 0 = (0gβπΊ) β β’ (π β π β 0 = (0gβπ)) | ||
Theorem | tngmulr 24377 | The ring multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ Β· = (.rβπΊ) β β’ (π β π β Β· = (.rβπ)) | ||
Theorem | tngmulrOLD 24378 | Obsolete proof of tngmulr 24377 as of 31-Oct-2024. The ring multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (πΊ toNrmGrp π) & β’ Β· = (.rβπΊ) β β’ (π β π β Β· = (.rβπ)) | ||
Theorem | tngsca 24379 | The scalar ring of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ πΉ = (ScalarβπΊ) β β’ (π β π β πΉ = (Scalarβπ)) | ||
Theorem | tngscaOLD 24380 | Obsolete proof of tngsca 24379 as of 31-Oct-2024. The scalar ring of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (πΊ toNrmGrp π) & β’ πΉ = (ScalarβπΊ) β β’ (π β π β πΉ = (Scalarβπ)) | ||
Theorem | tngvsca 24381 | The scalar multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ Β· = ( Β·π βπΊ) β β’ (π β π β Β· = ( Β·π βπ)) | ||
Theorem | tngvscaOLD 24382 | Obsolete proof of tngvsca 24381 as of 31-Oct-2024. The scalar multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (πΊ toNrmGrp π) & β’ Β· = ( Β·π βπΊ) β β’ (π β π β Β· = ( Β·π βπ)) | ||
Theorem | tngip 24383 | The inner product operation of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ , = (Β·πβπΊ) β β’ (π β π β , = (Β·πβπ)) | ||
Theorem | tngipOLD 24384 | Obsolete proof of tngip 24383 as of 31-Oct-2024. The inner product operation of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (πΊ toNrmGrp π) & β’ , = (Β·πβπΊ) β β’ (π β π β , = (Β·πβπ)) | ||
Theorem | tngds 24385 | The metric function of a structure augmented with a norm. (Contributed by Mario Carneiro, 3-Oct-2015.) (Proof shortened by AV, 29-Oct-2024.) |
β’ π = (πΊ toNrmGrp π) & β’ β = (-gβπΊ) β β’ (π β π β (π β β ) = (distβπ)) | ||
Theorem | tngdsOLD 24386 | Obsolete proof of tngds 24385 as of 29-Oct-2024. The metric function of a structure augmented with a norm. (Contributed by Mario Carneiro, 3-Oct-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (πΊ toNrmGrp π) & β’ β = (-gβπΊ) β β’ (π β π β (π β β ) = (distβπ)) | ||
Theorem | tngtset 24387 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 3-Oct-2015.) |
β’ π = (πΊ toNrmGrp π) & β’ π· = (distβπ) & β’ π½ = (MetOpenβπ·) β β’ ((πΊ β π β§ π β π) β π½ = (TopSetβπ)) | ||
Theorem | tngtopn 24388 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (πΊ toNrmGrp π) & β’ π· = (distβπ) & β’ π½ = (MetOpenβπ·) β β’ ((πΊ β π β§ π β π) β π½ = (TopOpenβπ)) | ||
Theorem | tngnm 24389 | The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (πΊ toNrmGrp π) & β’ π = (BaseβπΊ) & β’ π΄ β V β β’ ((πΊ β Grp β§ π:πβΆπ΄) β π = (normβπ)) | ||
Theorem | tngngp2 24390 | A norm turns a group into a normed group iff the generated metric is in fact a metric. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (πΊ toNrmGrp π) & β’ π = (BaseβπΊ) & β’ π· = (distβπ) β β’ (π:πβΆβ β (π β NrmGrp β (πΊ β Grp β§ π· β (Metβπ)))) | ||
Theorem | tngngpd 24391* | Derive the axioms for a normed group from the axioms for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (πΊ toNrmGrp π) & β’ π = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π:πβΆβ) & β’ ((π β§ π₯ β π) β ((πβπ₯) = 0 β π₯ = 0 )) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦))) β β’ (π β π β NrmGrp) | ||
Theorem | tngngp 24392* | Derive the axioms for a normed group from the axioms for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (πΊ toNrmGrp π) & β’ π = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ 0 = (0gβπΊ) β β’ (π:πβΆβ β (π β NrmGrp β (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ βπ¦ β π (πβ(π₯ β π¦)) β€ ((πβπ₯) + (πβπ¦)))))) | ||
Theorem | tnggrpr 24393 | If a structure equipped with a norm is a normed group, the structure itself must be a group. (Contributed by AV, 15-Oct-2021.) |
β’ π = (πΊ toNrmGrp π) β β’ ((π β π β§ π β NrmGrp) β πΊ β Grp) | ||
Theorem | tngngp3 24394* | Alternate definition of a normed group (i.e., a group equipped with a norm) without using the properties of a metric space. This corresponds to the definition in N. H. Bingham, A. J. Ostaszewski: "Normed versus topological groups: dichotomy and duality", 2010, Dissertationes Mathematicae 472, pp. 1-138 and E. Deza, M.M. Deza: "Dictionary of Distances", Elsevier, 2006. (Contributed by AV, 16-Oct-2021.) |
β’ π = (πΊ toNrmGrp π) & β’ π = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ πΌ = (invgβπΊ) β β’ (π:πβΆβ β (π β NrmGrp β (πΊ β Grp β§ βπ₯ β π (((πβπ₯) = 0 β π₯ = 0 ) β§ (πβ(πΌβπ₯)) = (πβπ₯) β§ βπ¦ β π (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦)))))) | ||
Theorem | nrmtngdist 24395 | The augmentation of a normed group by its own norm has the same distance function as the normed group (restricted to the base set). (Contributed by AV, 15-Oct-2021.) |
β’ π = (πΊ toNrmGrp (normβπΊ)) & β’ π = (BaseβπΊ) β β’ (πΊ β NrmGrp β (distβπ) = ((distβπΊ) βΎ (π Γ π))) | ||
Theorem | nrmtngnrm 24396 | The augmentation of a normed group by its own norm is a normed group with the same norm. (Contributed by AV, 15-Oct-2021.) |
β’ π = (πΊ toNrmGrp (normβπΊ)) β β’ (πΊ β NrmGrp β (π β NrmGrp β§ (normβπ) = (normβπΊ))) | ||
Theorem | tngngpim 24397 | The induced metric of a normed group is a function. (Contributed by AV, 19-Oct-2021.) |
β’ π = (πΊ toNrmGrp π) & β’ π = (normβπΊ) & β’ π = (BaseβπΊ) & β’ π· = (distβπ) β β’ (πΊ β NrmGrp β π·:(π Γ π)βΆβ) | ||
Theorem | isnrg 24398 | A normed ring is a ring with a norm that makes it into a normed group, and such that the norm is an absolute value on the ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (normβπ ) & β’ π΄ = (AbsValβπ ) β β’ (π β NrmRing β (π β NrmGrp β§ π β π΄)) | ||
Theorem | nrgabv 24399 | The norm of a normed ring is an absolute value. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (normβπ ) & β’ π΄ = (AbsValβπ ) β β’ (π β NrmRing β π β π΄) | ||
Theorem | nrgngp 24400 | A normed ring is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β NrmRing β π β NrmGrp) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |