Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,555 to 1,560 of 2,569 results.
LinearPMap.IsClosable.defectNumber_const
Mathematical statement
The defect number is constant on each connected component of the regularity domain.
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsClosed.add_continuous
Mathematical statement
Closedness is preserved upon adding a continuous operator.
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsClosed.resolventSet_eq
Mathematical statement
For a closed operator the continuity of the resolvent is redundant in the definition of the resolvent set.
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsClosed.resolventSet_eq'
Mathematical statement
For a closed operator the resolvent set consists of those regular points for which the defect number is zero.
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsClosed.spectrum_eq
Project documentation
The continuous spectrum, σᶜ, of a partial linear map. A complex number z is in σᶜ T iff the range of T - z • 1 is not closed. -/ def continuousSpectrum (T : H →ₗ.[ℂ] H) : Set ℂ := {z : ℂ | ¬root.IsClosed ((T - z • 1).toFun.range : Set H)} @[inherit_doc continuousSpectrum] scoped notation "σᶜ" => continuousSpectrum lemma continuousSpectrum_eq (T...
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsFormalAdjoint.unitaryConj
Mathematical statement
Unitary conjugation preserves formal adjointness. If A is a formal adjoint of B, then u A u⁻¹ is a formal adjoint of u B u⁻¹. Unitary conjugation preserves symmetry when A = B.
Source project: Physlib
Person-level attribution pending.