exists_subset_injOn_subset_range_eq

English

If r ⊆ s and f injOn r, then there exists u ⊇ r, u ⊆ s with f''u = f''s and f injOn u.

Русский

Если r ⊆ s и f инъективна на r, то существует u ⊇ r, u ⊆ s такое что f''u = f''s и f инъективна на u.

LaTeX

$$$\\exists u: Set\\alpha, r \\subseteq u \\subseteq s ∧ f''u = f''s ∧ InjOn f u$$$

Lean4

theorem exists_subset_injOn_subset_range_eq {r : Set α} (hinj : InjOn f r) (hrs : r ⊆ s) :
    ∃ u : Set α, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u :=
  by
  obtain ⟨u, hru, hus, h⟩ := hinj.bijOn_image.exists_extend_of_subset hrs (image_mono hrs) Subset.rfl
  exact ⟨u, hru, hus, h.image_eq, h.injOn⟩

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