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 591 research declarations. Search 10,000 more complete Mathlib declarations.
591 results
Clear filtersLinearPMap.IsClosable.add_continuous
Plain-language statement
Closability is preserved upon adding a continuous operator.
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsClosable.defectNumber_const
Plain-language 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
Plain-language statement
Closedness is preserved upon adding a continuous operator.
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsClosed.resolventSet_eq
Plain-language 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'
Plain-language 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.