image_invFunOn_image — Mathlib

English

If f is surjective on s to t, then the image under f of the inverse image of a subset r of t equals r.

Русский

Если f сюръективна с s на t, то образ f от invFunOn s '' r равен r для любого r ⊆ t.

LaTeX

$$$[\\text{Nonempty }\\alpha] \\ SurjOn f s t \\rightarrow f '' (f.invFunOn s '' r) = r$$$

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 [Nonempty α] (hf : SurjOn f s t) : f '' (f.invFunOn s '' t) = t :=
  hf.rightInvOn_invFunOn.image_image

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