Theorems · Theorem · operator theory

IsSelfAdjoint.dense_domain

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {A : E →ₗ.[𝕜] E}, IsSelfAdjoint A → Dense ↑A.domain

Every self-adjoint LinearPMap has dense domain. This is not true by definition since we define the adjoint without the assumption that the domain is dense, but the choice of the junk value implies that a LinearPMap cannot be self-adjoint if it does not have dense domain.

Defined in

Mathlib.Analysis.InnerProductSpace.LinearPMap

Cited by

1 results in Mathlib

Foundations

Depth 192 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceCompleteSpace