invFunOn_eq

Mathlib.Data.Set.Function

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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