Skip to content

Notation inconsistency in topology_structure.v #1803

@agontard

Description

@agontard

The following three objects named open/op should have the same type:

Definition nbhs_of_open (T : Type) (op : set T -> Prop) (p : T) (A : set T) :=

Metadata

Metadata

Assignees

No one assigned

    Labels

    renaming/refactoring 🔧This is about a renaming or refactoring in the library

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions