Skip to content

Can be weakened to realFieldType #1879

New issue
New issue
Open
#1881
Open
Can be weakened to realFieldType#1879
#1881
Labels
enhancement ✨This issue/PR is about adding new features enhancing the library
Milestone
1.16.0
@affeldt-aist

Description

@affeldt-aist
affeldt-aist
opened on Mar 5, 2026

analysis/theories/topology_theory/num_topology.v

Line 377 in 85fa9f6

Lemma lt_nbhsl {R : realType} (x a : R) : x < a ->

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancement ✨This issue/PR is about adding new features enhancing the library

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions