English
There exists a NormedSpace.Core structure on E over ℂ compatible with the given inner product, with field data: norm_nonneg, norm_eq_zero_iff, norm_smul, norm_triangle.
Русский
Существует структура NormedSpace.Core на E над ℂ, совместимая с данным вложенным произведением, удовлетворяющая поля норм: неотрицательность, нулиння, нормирование скаляра и треугольник.
LaTeX
$$$\\text{NormedSpace.Core} \\; \\mathbb{C}, E\\;\\text{ exists with }\\; \\text{norm\_nonneg},\\; \\text{norm\_eq\_zero\_iff},\\; \\text{norm\_smul},\\; \\text{norm\_triangle}$$$
Lean4
/-- This allows us to get `NormedAddCommGroup` and `NormedSpace` instances on `E` via
`NormedAddCommGroup.ofCore` and `NormedSpace.ofCore`. -/
theorem normedSpaceCore : NormedSpace.Core ℂ E
where
norm_nonneg _ := (CStarModule.norm_nonneg A)
norm_eq_zero_iff x := norm_zero_iff A x
norm_smul c x := by simp [norm_eq_sqrt_norm_inner_self (A := A), norm_smul, ← mul_assoc]
norm_triangle x y := CStarModule.norm_triangle A x y
