invFunOn_mem — Mathlib

English

If there exists a in s with f a = b, then invFunOn f s b lies in s and f(invFunOn f s b) = b.

Русский

Если существует a∈s такое, что f a = b, то invFunOn f s b находится в s и выполняется равенство f(invFunOn f s b) = b.

LaTeX

$$$$\\big(\\exists a \\in s, f a = b\\big) \\Rightarrow \\operatorname{invFunOn} f s b \\in s \\land f(\\operatorname{invFunOn} f s b) = b.$$$$

Lean4

theorem invFunOn_mem (h : ∃ a ∈ s, f a = b) : invFunOn f s b ∈ s :=
  (invFunOn_pos h).left

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