Skip to content

Can we hide the invocation to val? #2138

Open
Open
Can we hide the invocation to val?#2138
Labels
question ❓There is an unanswered question here
Milestone
1.20.0

Description

@affeldt-aist
affeldt-aist
opened on Oct 21, 2026

analysis/theories/functional_analysis/hahn_banach_theorem.v

Line 386 in e4a9991

seminorm_of p & forall z : F', f z <= p (val z)) ->

This was a question raised during the development of PR #1963

fyi: @CohenCyril @mkerjean

Activity

  1. affeldt-aist
    added this to the 1.20.0 milestone on Oct 21, 2026
  2. affeldt-aist
    added
    question ❓There is an unanswered question here
    on Oct 21, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    question ❓There is an unanswered question here

    Type

    No type

    Projects

    No projects

      Milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions