ReflexiveFixedPoints
DefinitionFor a real normed vector space X, with universe-polymorphic type X, CanonicallyReflexive(X) is a defined proposition (not an asserted theorem) stating that the canonical embedding of X into its continuous double dual, the map sending each x to the evaluation functional on continuous linear functionals f given by f(x), is surjective. In other words, every continuous linear functional on the continuous dual of X is evaluation at some point of X. The block contains only this one definition and no results about which spaces satisfy it.
Definition code
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/ReflexiveFixedPoints.lean; bytes 16..347
-- Kind: block; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.
import Mathlib
namespace OAI
noncomputable section
namespace ReflexiveFixedPoints
universe u
variable (X : Type u) [NormedAddCommGroup X] [NormedSpace ℝ X]
/-- Surjectivity of the canonical map into the continuous bidual. -/
def CanonicallyReflexive : Prop :=
Function.Surjective (NormedSpace.inclusionInDoubleDual ℝ X)
variable {X}
end ReflexiveFixedPoints
end
end OAI
Source
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.