Theorem compRel_left_mono

Modification history

2025-07-31 09:17
Mathlib/Topology/UniformSpace/Defs.lean
feat(gcongr): also use more general lemmas, closing extra goals with rfl (#26907) …
Deleted compRel_left_monoView on Github →
2025-06-11 23:54
Mathlib/Topology/UniformSpace/Defs.lean
chore: remove last use of `mono` tactic (#25698) …
Added compRel_left_monoView on Github →