invFunOn_neg — Mathlib

English

If there does not exist a in s with f a = b, then invFunOn f s b equals an arbitrary choice from a nonempty domain.

Русский

Если не существует a∈s такого, что f a = b, то invFunOn f s b равно произвольному выбору из непустого множества.

LaTeX

$$$$\\neg \\exists a\\in s, f a = b \\Rightarrow \\operatorname{invFunOn} f s b = \\text{arbitrary choice}. $$$$

Lean4

theorem invFunOn_neg (h : ¬∃ a ∈ s, f a = b) : invFunOn f s b = Classical.choice ‹Nonempty α› := by
  rw [invFunOn, dif_neg h]

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