image — Mathlib

English

If f is injective, then s ≃ f''s for any set s.

Русский

Если функция инъективна, то для любого множества s выполняется биекция s ≃ f''s.

LaTeX

$$s \cong f''s$$

Lean4

/-- If `f` is an injective function, then `s` is equivalent to `f '' s`. -/
@[simps! apply]
protected noncomputable def image {α β} (f : α → β) (s : Set α) (H : Injective f) : s ≃ f '' s :=
  Equiv.Set.imageOfInjOn f s H.injOn

Похожие утверждения