{T P : E →ₗ[ℂ] E} {s c : ℝ} (hne : (sectorRayleighSet T P s).Nonempty) (hlb : ∀ x : E, ‖x‖ = 1 → x ∈ paritySector P s → c ≤ rayleigh T x) : c ≤ sectorGround T P s

Initializing...

{T P : E →ₗ[ℂ] E} {s c : ℝ} (hne : (sectorRayleighSet T P s).Nonempty) (hlb : ∀ x : E, ‖x‖ = 1 → x ∈ paritySector P s → c ≤ rayleigh T x) : c ≤ sectorGround T P s · Prove2Me