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,567 to 1,572 of 2,569 results.
LinearPMap.IsSymmetric.regularityDomain_isConnected_iff
Mathematical statement
The regularity domain of a symmetric operator is connected iff it contains a real number.
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsUnbounded.orthogonal_adjoint_sub_ker
Mathematical statement
(T† - conj z • 1).kerᗮ = (T.closure - z • 1).range
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsUnbounded.orthogonal_closure_sub_range
Mathematical statement
(T.closure - z • 1).rangeᗮ = (T† - conj z • 1).ker
Source project: Physlib
Person-level attribution pending.
LinearPMap.mem_regularityDomain_iff
Mathematical statement
z is a regular point for T iff T - z • 1 has a continuous (equivalently, bounded) inverse.
Source project: Physlib
Person-level attribution pending.
LinearPMap.numericalRange_convex
Project documentation
The Toeplitz-Hausdorff theorem.
Source project: Physlib
Person-level attribution pending.
LinearPMap.resolvent_sub
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.