image_invFunOn_image_of_subset — Mathlib

English

If f is surjective on s onto t and r ⊆ t, then the image under f of the inverse image of r on s equals r.

Русский

Если f отображает s на t и r ⊆ t, то образ f от invFunOn(s, r) равен r.

LaTeX

$$$[\\text{Nonempty }\\alpha] \\ SurjOn f s t \\rightarrow f '' (f.invFunOn s '' r) = r$ \\\\ (для любого r ⊆ t)$$

Lean4

/-- This lemma is a special case of `rightInvOn_invFunOn.image_image'`; it may make more sense
to use the other lemma directly in an application. -/
theorem image_invFunOn_image_of_subset [Nonempty α] {r : Set β} (hf : SurjOn f s t) (hrt : r ⊆ t) :
    f '' (f.invFunOn s '' r) = r :=
  hf.rightInvOn_invFunOn.image_image' hrt

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