Skip to content

Differentiable maps from proper closed intervals in the reals to a normed real vector space#1978

Open
lowasser wants to merge 3 commits into
UniMath:masterfrom
lowasser:differentiable-functional-analysis
Open

Differentiable maps from proper closed intervals in the reals to a normed real vector space#1978
lowasser wants to merge 3 commits into
UniMath:masterfrom
lowasser:differentiable-functional-analysis

Conversation

@lowasser

@lowasser lowasser commented Jun 9, 2026

Copy link
Copy Markdown
Collaborator

Lots more properties to prove, but we start with a definition and showing that differentiability is a proposition.

Eventually I think we'd like to redefine derivatives of real-valued maps in terms of this more general definition, presumably also defining normed algebras so we can define the product rule. But this is a reasonable start.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant