exists_image_eq_injOn_of_subset_range

English

If t ⊆ range f, there exists s with f''s = t and f injOn s.

Русский

Если t ⊆ range f, существует s ⊆ домен, такое что f''s = t и f инъективна на s.

LaTeX

$$$t \\subseteq \\mathrm{range}(f) \\Rightarrow \\exists s, f''s = t \\land InjOn f s$$$

Lean4

theorem exists_image_eq_injOn_of_subset_range (ht : t ⊆ range f) : ∃ s, f '' s = t ∧ InjOn f s :=
  image_preimage_eq_of_subset ht ▸ exists_image_eq_and_injOn _ _

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