Theorem AbstractCompletion.extend_def

Modification history

2024-09-29 00:04

Mathlib/Topology/UniformSpace/AbstractCompletion.lean

chore: Rename `DenseInducing` to `IsDenseInducing` (#17208) …

Modified AbstractCompletion.extend_def View on Github →

2023-02-12 22:01

Mathlib/Topology/UniformSpace/AbstractCompletion.lean

feat: port Topology.UniformSpace.AbstractCompletion (#2238)

Added AbstractCompletion.extend_def View on Github →