Theorems · Definition · functional analysis

ClosedSubmodule.symplComp

{H : Type u_1} →
  [inst : NormedAddCommGroup H] → [ipc : InnerProductSpace ℂ H] → ClosedSubmodule ℝ H → ClosedSubmodule ℝ H

The symplectic complement of a closed submodule with respect to ⟪⬝, ⬝⟫.im, defined as the image of mulI and orthogonal. The proof that this is the symplectic complement is given by mem_symplComp_iff.

Defined in

Mathlib.Analysis.InnerProductSpace.StandardSubspace

Cited by

7 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpace