Theorem AbstractCompletion.compare_comp_eq_compare

Modification history

2025-08-04 10:34

Mathlib/Topology/UniformSpace/AbstractCompletion.lean

chore(AbstractCompletion): universe polymorphism (#27762)

Modified AbstractCompletion.compare_comp_eq_compare View on Github →

2024-07-15 19:24

Mathlib/Topology/UniformSpace/AbstractCompletion.lean

feat(Topology/UniformSpace/AbstractCompletion):add comparison lemma (#12979) …

Added AbstractCompletion.compare_comp_eq_compare View on Github →