Theorems · Theorem · functional analysis

IsCoercive.range_eq_top

∀ {V : Type u} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : CompleteSpace V]
  {B : V →L[ℝ] V →L[ℝ] ℝ}, IsCoercive B → (↑(InnerProductSpace.continuousLinearMapOfBilin B)).range = ⊤

Defined in

Mathlib.Analysis.InnerProductSpace.LaxMilgram

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceCompleteSpace