Theorem uniformContinuous_inr

Modification history

2026-07-08 10:17

Mathlib/Topology/UniformSpace/Basic.lean

feat(Topology/UniformSpace): tag `UniformContinuous` with `@[fun_prop]` (#41019) …

Modified uniformContinuous_inr View on Github →

2023-02-04 08:44

Mathlib/Topology/UniformSpace/Basic.lean

feat: port Topology.UniformSpace.UniformEmbedding (#2038)

Added uniformContinuous_inr View on Github →