Theorems · Definition · general topology

Set.InjOn.toPartialEquiv

{α : Type u_1} → {β : Type u_2} → [Nonempty α] → (f : α → β) → (s : Set α) → Set.InjOn f s → PartialEquiv α β

A map injective on a subset of its domain provides a partial equivalence.

Defined in

Mathlib.Logic.Equiv.PartialEquiv

Cited by

2 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Nonempty