mapsTo_invFunOn — Mathlib

English

Let f be a function between types and s ⊆ α, t ⊆ β. If f maps s onto t, then the restricted inverse on s sends every y ∈ t back into s.

Русский

Пусть f: α → β и s ⊆ α, t ⊆ β. Если f отображает s на t, то частная обратная функция invFunOn f s отображает каждый элемент t обратно в s.

LaTeX

$$$[\\text{Nonempty }\\alpha] \\\\ SurjOn f\ \, s\ t \\\\Rightarrow \\\\ mapsTo (invFunOn\, f\, s)\ \, t\ \, s$$$

Lean4

theorem mapsTo_invFunOn [Nonempty α] (h : SurjOn f s t) : MapsTo (invFunOn f s) t s := fun _y hy =>
  mem_preimage.2 <| invFunOn_mem <| h hy

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