invFunOn_pos — Mathlib

English

If f is a bijection between s and t, then invFunOn f s is an inverse-on relation for f on s,t.

Русский

Если f — биекция между s и t, то invFunOn f s образует взаимную обратимость между s и t.

LaTeX

$$$$\\forall [Nonempty\\ α], \\operatorname{BijOn}(f, s, t) \\Rightarrow \\operatorname{InvOn}(\\operatorname{invFunOn} f s, f, s, t).$$$$

Lean4

theorem invFunOn_pos (h : ∃ a ∈ s, f a = b) : invFunOn f s b ∈ s ∧ f (invFunOn f s b) = b :=
  by
  rw [invFunOn, dif_pos h]
  exact Classical.choose_spec h

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