image_eq_iff_surjOn_mapsTo — Mathlib

English

The image equality f''s = t is equivalent to SurjOn f s t and MapsTo f s t.

Русский

Равенство образа f''s = t эквивалентно условию SurjOn f s t и MapsTo f s t.

LaTeX

$$$ f''s = t \iff (\mathrm{SurjOn} f s t \land \mathrm{MapsTo} f s t) $$$

Lean4

theorem image_eq_iff_surjOn_mapsTo : f '' s = t ↔ s.SurjOn f t ∧ s.MapsTo f t :=
  by
  refine ⟨?_, fun h => h.1.image_eq_of_mapsTo h.2⟩
  rintro rfl
  exact ⟨s.surjOn_image f, s.mapsTo_image f⟩

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