mapsTo_compl — Mathlib

English

The statement image_eq_iff_surjOn_mapsTo expresses that f''s = t is equivalent to SurjOn f s t and MapsTo f s t.

Русский

Утверждение image_eq_iff_surjOn_mapsTo выражает, что 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 mapsTo_compl (h : SurjOn f s t) (h' : Injective f) : MapsTo f sᶜ tᶜ := fun _ hs ht =>
  let ⟨_, hx', HEq⟩ := h ht
  hs <| h' HEq ▸ hx'

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