Shortcut instances for concrete real normed spaces

Instance resolution on a concrete function space (an Lp space, a closed submodule of a product of Lp spaces, a space of continuous linear maps between them) has to rediscover each derived structure such as AddCommMonoid, Module ℝ or TopologicalSpace by search. On such carriers the search explores many failing subobject and algebra branches before it succeeds, and it is repeated in every declaration that mentions the space.

The commands of this file record, for a given carrier X, the instances that resolution currently finds, and register them as instances of X itself:

• normed_group_shortcut_instances p binders : X records NormedAddCommGroup X and the additive, metric and topological structures derived from it;
• normed_space_shortcut_instances p binders : X records NormedSpace ℝ X and the scalar structures derived from it;
• real_normed_space_shortcut_instances p binders : X does both.

Each generated declaration is named p.inst followed by the class name. Each reducible definition unfolds to the instance term captured when its body is elaborated. The generated theorem aliases have proposition-valued targets; proof irrelevance applies at a fixed target with fixed data parameters. Within one group or scalar batch, the declarations are elaborated before that batch's final attribute [instance] command. The combined command completes and registers the group batch before elaborating the scalar batch. Later invocations and imported shortcut modules can therefore see aliases registered by earlier batches.

SeminormedAddCommGroup X is projected from the normed group selected in the same group batch. The scalar batch is elaborated after those group aliases are registered. The generated declarations are then available as instances for later queries on X. This capture order alone does not establish that the complete shortcut set reproduces the instance terms from an environment with no shortcuts, or that every direct alias is definitionally equal to every higher-class projection on every carrier.

def «commandNormed_group_shortcut_instances__:_» : Lean.ParserDescr

normed_group_shortcut_instances p binders : X registers the instances currently found for NormedAddCommGroup X and for the additive, metric and topological structures of X as instances named p.inst followed by the class name.

Equations

• One or more equations did not get rendered due to their size.

def «commandNormed_space_shortcut_instances__:_» : Lean.ParserDescr

normed_space_shortcut_instances p binders : X registers the instances currently found for NormedSpace ℝ X and for the scalar structures of X as instances named p.inst followed by the class name. It is meant to follow normed_group_shortcut_instances p binders : X.

Equations

• One or more equations did not get rendered due to their size.

def «commandReal_normed_space_shortcut_instances__:_» : Lean.ParserDescr

real_normed_space_shortcut_instances p binders : X combines normed_group_shortcut_instances p binders : X and normed_space_shortcut_instances p binders : X.

Equations

• One or more equations did not get rendered due to their size.