English
If A is a self-adjoint LinearPMap, then its domain is dense in the ambient space E.
Русский
Пусть A является сам-сопряжённым линейным частичным отображением; тогда область определения A плотно сидит внутри пространства E.
LaTeX
$$$\\text{IsSelfAdjoint}(A) \\Rightarrow \\operatorname{Dense}(A.\\mathrm{domain})$$$
Lean4
/-- 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. -/
theorem _root_.IsSelfAdjoint.dense_domain (hA : IsSelfAdjoint A) : Dense (A.domain : Set E) :=
by
by_contra h
rw [isSelfAdjoint_def] at hA
have h' : A.domain = ⊤ := by
rw [← hA, Submodule.eq_top_iff']
intro x
rw [mem_adjoint_domain_iff, ← hA]
refine (innerSL 𝕜 x).cont.comp ?_
simp only [adjoint, h]
exact continuous_const
simp [h'] at h
