Skip to content

better names for the fields of pseudo-metric spaces #868

@affeldt-aist

Description

@affeldt-aist

analysis/theories/topology.v

Lines 4544 to 4547 in 0e392b5

ax1 : forall x (e : R), 0 < e -> ball x e x ;
ax2 : forall x y (e : R), ball x e y -> ball y e x ;
ax3 : forall x y z e1 e2, ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z;
ax4 : entourage = entourage_ ball

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

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions