partialInv_left

Mathlib.Logic.Function.Basic

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

English

If f is injective, then for every x, partialInv f (f x) = some x.

Русский

Если f инъективна, тогда для каждого x выполнено partialInv f (f x) = some x.

LaTeX

$$$ \text{Injective}(f) \rightarrow \forall x, \mathrm{partialInv}(f)(f(x)) = \mathrm{Some}(x) $$$

Lean4

theorem partialInv_left {α β} {f : α → β} (I : Injective f) : ∀ x, partialInv f (f x) = some x :=
  isPartialInv_left (partialInv_of_injective I)

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

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

Разделы

Аффилиация

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