invFun_neg

Mathlib.Logic.Function.Basic

URI: https://scilib.ai/kg/mathlib#Function.invFun_neg

English

If there is no a with f a = b, then invFun f b equals a fixed default element a0 of α.

Русский

Если не существует a с f a = b, то invFun f b равняется фиксированному элементу a0 множества α.

LaTeX

$$$ \neg \exists a, f(a) = b \rightarrow \mathrm{invFun}(f,b) = a_0 $$$

Lean4

theorem invFun_neg (h : ¬∃ a, f a = b) : invFun f b = Classical.choice ‹_› :=
  dif_neg h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru