Theorems · Definition · functional analysis

PreInnerProductSpace.toCore

{𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [c : InnerProductSpace 𝕜 E] → PreInnerProductSpace.Core 𝕜 E

Define PreInnerProductSpace.Core from InnerProductSpace. Defined to reuse lemmas about PreInnerProductSpace.Core for PreInnerProductSpaces. Note that the Seminorm instance provided by PreInnerProductSpace.Core.norm is propositionally but not definitionally equal to the original norm.

Defined in: Mathlib.Analysis.InnerProductSpace.Defs
Cited by: 2 results in Mathlib
Foundations: Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: RCLike SeminormedAddCommGroup InnerProductSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

InnerProductSpacestatement and proof · cited by 3,523
RCLikestatement and proof · cited by 2,829
SeminormedAddCommGroupstatement and proof · cited by 2,671
PreInnerProductSpace.Corestatement · cited by 46
InnerProductSpace.conj_inner_symmproof · cited by 2
InnerProductSpace.smul_leftproof · cited by 1
InnerProductSpace.add_leftproof · cited by 1

Cited by2

Results whose statement or proof uses this declaration.

norm_inner_le_normproof · cited by 14
inner_self_nonnegproof · cited by 6