Theorem CompHaus.mono_iff_injective

Modification history

2024-07-16 22:20

Mathlib/Topology/Category/CompHaus/Basic.lean

refactor(Topology/Category): refactor CompHaus.Basic (#13908) …

Deleted CompHaus.mono_iff_injective View on Github →

2023-04-27 23:18

Mathlib/Topology/Category/CompHaus/Basic.lean

feat: Port Topology.Category.CompHaus.Basic (#3688) …

Added CompHaus.mono_iff_injective View on Github →