Skip to content

generalize Order_isNbhs #1779

New issue
New issue
Open
Open
generalize Order_isNbhs#1779
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 Nov 27, 2025

analysis/theories/topology_theory/order_topology.v

Line 25 in 5e727ce

(** TODO: generalize this to a preOrder once that's available *)

when dropping support for MathComp < 2.5

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