Documentation
LeanPool
.
RlTheoryInLean
.
Analysis
.
Normed
.
Group
.
Basic
Search
return to top
source
Imports
Init
Mathlib.Algebra.Order.Ring.Basic
Mathlib.Analysis.Normed.Group.Basic
Imported by
norm_add_sq_le_norm_sq_add_norm_sq
LeanPool.RlTheoryInLean.Analysis.Normed.Group.Basic
#
source
theorem
norm_add_sq_le_norm_sq_add_norm_sq
{
E
:
Type
u_1}
[
SeminormedAddGroup
E
]
(
x
y
:
E
)
:
‖
x
+
y
‖
^
2
≤
2
*
‖
x
‖
^
2
+
2
*
‖
y
‖
^
2