exists_subset_bijOn — Mathlib

English

For any s and f, there exists a subset s' of s such that f restricted to s' is bijective onto f(s).

Русский

Для любых s и f существует подмножество s' ⊆ s, такое что ограничение f на s' биективно отображает s на f(s).

LaTeX

$$$\\exists s' \\subseteq s, BijOn\ f\ s' (f '' s)$$$

Lean4

theorem exists_subset_bijOn : ∃ s' ⊆ s, BijOn f s' (f '' s) :=
  surjOn_iff_exists_bijOn_subset.mp (surjOn_image f s)

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