surjOn_compl — Mathlib

English

If Set.SurjOn f s t and MapsTo f s t, then s.EqOn (g₁ ∘ f) (g₂ ∘ f) iff t.EqOn g₁ g₂.

Русский

Если SurjOn f s t и MapsTo f s t, то равенство функций после композиции эквивалентно равенству на t

LaTeX

$$$ (\mathrm{EqOn}(g_1\circ f)(g_2\circ f)\; s) \iff (t\mathrm{EqOn} g_1 g_2) $$$

Lean4

theorem surjOn_compl (h : MapsTo f s t) (h' : Surjective f) : SurjOn f sᶜ tᶜ :=
  h'.forall.2 fun _ ht => (mem_image_of_mem _) fun hs => ht (h hs)

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