Theorems · Definition · logic and foundations

Equiv.Set.image

{α : Type u_3} → {β : Type u_4} → (f : α → β) → (s : Set α) → Function.Injective f → ↑s ≃ ↑(f '' s)

If f is an injective function, then s is equivalent to f '' s.

Defined in

Mathlib.Logic.Equiv.Set

Cited by

15 results in Mathlib

Foundations

Depth 13 from the axioms · uses Classical.choice