invOn_invFunOn — Mathlib

English

If f is surjective on s to t, then invFunOn f s composed with f gives an inverse-on relation from invFunOn f s to f on the image of t.

Русский

Если f сюръективна, то invFunOn f s и f образуют инверсную структуру на соответствующих множествах.

LaTeX

$$$$\\operatorname{SurjOn}(f, s, t) \\Rightarrow \\operatorname{InvOn}(\\operatorname{invFunOn} f s, f, \\operatorname{image}(\\operatorname{invFunOn} f s, t), t).$$$$

Lean4

theorem invOn_invFunOn [Nonempty α] (h : BijOn f s t) : InvOn (invFunOn f s) f s t :=
  ⟨h.injOn.leftInvOn_invFunOn, h.surjOn.rightInvOn_invFunOn⟩

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